proposition: Lemma aleph_pr13 n: ordinalp n -> \aleph (osucc n) <c \2c ^c (\2c ^c (\aleph n)).
proof: Proof. move => on. have son:= OS_succ on. have cas:= CS_aleph son. have con := CS_aleph on. have icy:= CIS_aleph on. have ->: \2c ^c \aleph n = \2c ^c (coarse (\aleph n)). rewrite - {1} (csquare_inf icy). by apply: cpow_pr; fprops; rewrite /coarse cprod2_pr1; aw. apply: (clt_leT (cantor cas)). apply: (cpow_Meqle card2_nz); rewrite - card_setP - (aleph_succ_pr2 on). apply: surjective_cle. set E := \aleph n. pose f X := Yo ((worder X) /\ cardinal (substrate X) = E) (ordinal X) E. set T := (aleph_succ_comp n). have zT: inc E T. apply /setC_P; split; last by exact: (ordinal_irreflexive (proj1 con)). by move: (oclt (aleph_pr10c on)) => /oltP0 []. have oas:= OS_aleph son. have ta: lf_axiom f (\Po (coarse E)) (aleph_succ_comp n). move => t te; rewrite /f; Ytac h; last by exact. move: h => [h1 h2]. have oot:= (OS_ordinal h1). case: (oleT_el oas oot) => // le1. move: (ocle1 le1); rewrite (cardinal_of_ordinal h1). rewrite h2 (card_card cas) => le2. case: (cleNgt le2 (aleph_lt_ltc (oltS on))). move /oltP0: le1 => [_ _ lt1]. apply /setC_P; split => // le3. have: (ordinal t) <o E by apply /(oltP (proj1 con)). move /(ocle2P con oot). by rewrite (cardinal_of_ordinal h1) h2; move => [_]. exists (Lf f (\Po (coarse E)) T);saw. apply: lf_surjective => // x /(aleph_succ_P1 on) [pa pb]. have ox:= proj32 pa. have pg: cardinal x = E. apply: cleA; last by move: (ocle1 pa);rewrite (card_card con). move /(ocle2P cas ox): pb; rewrite - (cnextE on) => h. exact:(cnext_pr4 (proj1 icy) h). have [g [bg sg tg]]: exists g, bijection_prop g x E. by apply /card_eqP; rewrite (card_card con). have wox:=(ordinal_o_wor ox). have pc: substrate (ordinal_o x) = source g by rewrite ordinal_o_sr. move: (bg) => [[fg _] _]. have pd: function (ext_to_prod g g) by apply: ext_to_prod_f. have pe: sub (ordinal_o x) ((source g) \times (source g)). rewrite -pc; apply: sub_graph_coarse_substrate; fprops. have pf: sub (ordinal_o x) (source (ext_to_prod g g)). by rewrite /ext_to_prod; aw. move: (order_transportation bg (conj (proj1 wox) pc)). set o := Vfs _ _ => isg. exists o. apply /setP_P => t /(Vf_image_P pd pf) [u uo ->]. move: (pe _ uo) => up; rewrite (ext_to_prod_V2 fg fg up). move: up => /setX_P [_ p1 p2]; apply /setXp_P;split => //; Wtac. have es1: ordinal_o x \Is o by exists g. move: (worder_invariance es1 wox) => woE. have eq: x = ordinal o by symmetry;apply: ordinal_o_isu2 => //; apply: orderIS. rewrite /f Y_true //; split => //. rewrite - (cardinal_of_ordinal woE) - eq //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)