proposition: Lemma card_universe a: ordinalp a -> cardinal (universe (omega0 +o a)) = beth a.
proof: Proof. move => oa. pose hyp a:= cardinal (universe (omega0 +o a)) = beth a. case:(least_ordinal6 hyp oa); first by apply. set y := least_ordinal _ _;move => [oy hrec]; case. case: (ordinal_limA oy) => h. + by rewrite /hyp h (osum0r OS_omega) beth0 card_universe_omega. + move: h=> [z oz zv]; rewrite /hyp zv (beth_succ oz). rewrite - (osum2_succ OS_omega oz) (universe_succ (OS_sum2 OS_omega oz)). rewrite card_setP - cpowcr hrec //; rewrite zv; fprops. + rewrite /hyp. have ls:= osum_limit OS_omega h. rewrite (universe_limit ls); apply: cleA. apply: (cleT (csum_pr1_bis (omega0 +o y) universe)). rewrite/csumb; set f := Lg _ _. have csf: csum_of_small1 (beth y) f. rewrite /f; split; fprops; hnf; aw; move => i id; rewrite LgV//. move/(oltP (proj31 ls)): id => lio. case: (oleT_ee OS_omega (proj31_1 lio)) => sa. move: (odiff_pr sa) => [sc sd]. have sz: (i -o omega0) <o y. by apply:(osum_Meqltr sc (proj31 h) OS_omega); rewrite - sd. rewrite sd (hrec _ (olt_i sz)); exact: (beth_M sz). move:(sub_smaller (universe_inc2 sa)); rewrite card_universe_omega => sd. apply:(cle_ltT sd); rewrite /aleph0 - beth0; apply:beth_M. apply:(limit_pos h). have icb:= (beth_pr1 oy). move: (csum_of_small_b2 csf); rewrite - cprod2cr {2}/f Lgd. have ds: cardinal (omega0 +o y) <=c beth y. rewrite (osum_cardinal OS_omega oy). have ha:= (osi_gex (proj1 beth_normal) oy). have hb:= (oleT (limit_ge_omega h) ha). move: (csum_Mlele (ocle1 hb) (ocle1 ha)). by rewrite (card_card (proj1 icb)) (csum_inf1 icb). rewrite (cprod_inf ds icb) // => /card_nonempty => sz. exact: (omega_nz (proj1 (osum2_zero OS_omega oy sz))). rewrite (proj2 beth_normal _ h). apply: card_ub_sup; first by exact:CS_cardinal. move => i /funI_P [z zy ->]. rewrite - (hrec _ zy); apply: sub_smaller => t tu. apply/setUf_P; exists (omega0 +o z) => //; apply: olt_i. apply: (osum_Meqlt _ OS_omega); exact/oltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)