proposition: Lemma gimel_prop n (x:= \aleph n): ordinalp n -> [/\ (n = \0c -> \2c ^c x = gimel_fct x), (osuccp n) -> \2c ^c x = gimel_fct x, (limit_ordinal n -> cpow_less_ecb x -> \2c ^c x = \2c ^<c x *c gimel_fct x)& (limit_ordinal n -> not (cpow_less_ecb x) -> \2c ^c x = gimel_fct (\2c ^<c x))].
proof: Proof. move => on. have res1: n = \0c -> \2c ^c x = gimel_fct x. move => h; symmetry; apply: gimel_prop1. by rewrite /x h aleph0E; apply: regular_cardinal_omega. have res2: osuccp n -> \2c ^c x = gimel_fct x. move => [m om nm]; symmetry. move: (regular_initial_successor om); rewrite -nm;apply: gimel_prop1. move: (CIS_aleph on); rewrite -/x => icx. move: (cofinality_infinite_cardinal icx)(gimel_prop2 icx)(icx) => coi g2 [cx _]. have pa: limit_ordinal n -> infinite_c (\2c ^<c x). move => ln. have h:= (cpow_less_pr2 \2c (aleph_lt_ltc (limit_pos ln))). have ip2o:= (infinite_pow2 (CIS_aleph OS0)). exact (cle_inf_inf ip2o h). split => //. move=> ln cs; move: (infinite_pow2 icx) => ip2x. case: (equal_or_not x (\cf x)) => xcx. have rx: regular_cardinal x by apply /regular_cardinalP. rewrite (gimel_prop1 rx) cprodC; symmetry; apply cprod_inf => //. apply: (cpow_less_pr1 clt_02 cx). exact (infinite_nz (pa ln)). have si: singular_cardinal x by split => //; apply:nesym. rewrite - (cpow_less_pr10 si cs). symmetry; apply cprod_inf => //. apply: infinite_nz; apply: CIS_pow2 => //. move => ln nl. have paln:= (pa ln). rewrite /gimel_fct (cpow_less_pr6a icx). suff aux: \cf (\2c ^<c x) = \cf x by ue. have ox: ordinalp x by apply: OS_cardinal. have oy: ordinalp (\2c ^<c x) by move: paln => [pb _]; apply: OS_cardinal. move: (cofinality_rw ox) (cofinality_rw oy) => [qa qb qc] [qd qe qf]. have x1: forall t, t <c x -> \2c ^c t <c \2c ^<c x. move => t tx; split; first by apply: cpow_less_pr2. move => ub; case: nl; exists t => //. move => b b1 b2. move: (cpow_M2le b1) (cpow_less_pr2 \2c b2); rewrite - ub. apply:cleA. have x2: forall t, t <o \2c ^<c x -> exists2 u, t <=o \2c ^c u & u <c x. move => t tl. have ot:= proj31_1 tl. move /(ocle2P (proj1 paln) ot): tl => tl. case: (oleT_el OS_omega ot) => cto; last first. exists omega0. exact (oleT (proj1 cto) (proj1 (oclt (cantor CS_omega)))). rewrite - aleph0E; apply: aleph_lt_ltc. by move: ln => [_ ok _]; apply /oltP. move: (infinite_set_pr3 cto) => /infinite_setP ict. move: (cnext_pr1 (proj1 ict)) => []; set st := cnext (cardinal t). move=> sa sc sb; move: (sb _ tl) => sd. set sst:= Yo (cardinalp t) t st. have pc: t <=o sst. rewrite /sst; Ytac ct; first by apply: oleR. case: (oleT_ee ot (proj1 sa)) => // xx. by move: (ocle1 xx); rewrite -/st (card_card sa) =>/(cltNge sc). have sdd : sst <c \2c ^<c x. rewrite /sst; Ytac ct; first by rewrite - (card_card ct). split; [by apply: sd | move => bad ]. case: (p_or_not_p (exists2 u, u <c x & \2c ^c u = \2c ^<c x)) => H. by move: H => [u ua ub]; move: (x1 _ ua) => [_ xbad]. have bad2: forall w, w <c x -> \2c ^c w <=c (cardinal t). move=> w wc;apply: (cnext_pr4 (proj1 ict)); rewrite -/st bad; split. exact: (cpow_less_pr2 \2c wc). by move => eq; case: H; exists w. have bad3: \2c ^<c x <=c cardinal t. apply: card_ub_sup; first apply: CS_cardinal. by move=> i /funI_P [z zs ->]; apply: bad2; apply /(cardinals_ltP cx). case: (cltNge sc (cleT sd bad3)). suff: (exists2 u, sst <=c \2c ^c u & u <c x). move => [u /ocle p1 p2]; exists u => //; exact: (oleT pc p1). ex_middle bad; case: (cltNge sdd). have cs:= (proj31_1 sdd). apply:card_ub_sup; first exact cs. move =>i /funI_P [z /(cardinals_ltP cx) zx ->]. have c2: cardinalp (\2c ^c z) by fprops. by case: (cleT_ee cs c2) => // le4; case: bad; exists z. apply: oleA. move: (qb) => [f [[ff sf tf] cf]]. set g := Lf (fun z => \2c ^c (Vf f z)) (\cf x) (\2c ^<c x). have ta: lf_axiom (fun z => \2c ^c (Vf f z)) (\cf x) (\2c ^<c x). rewrite - sf; move => t ts /=; rewrite - cpowcr. set zz := cardinal _. have zzx: zz <c x by apply:colt1=> //;rewrite -tf; fprops. move: (cpow_less_pr2 \2c zzx) => [a1 a2 a3]. case: (ordinal_sub (OS_cardinal a1) (OS_cardinal a2) a3) => // eq1. by move: (proj2 (x1 _ zzx)); rewrite eq1. have fg: function g by apply: lf_function. apply: (qf _ qa); exists g. split; [ by hnf; rewrite /g; split => //; aw | move => t tp]. have tl: t <o (\2c ^<c x) by apply/oltP. move: (x2 _ tl) => [u u1 u2]. have ui: inc u x by move: (oclt u2) => /oltP0 [_ _]. move: (cf _ ui) => [z zx le2]; exists z => //. rewrite /g LfV//. have le3:= (ocle1 le2). move: (cpow_M2le le3); rewrite cpowcr cpowcr. move => le4; exact: (oleT u1 (ocle le4)). move: (qe) => [f [[ff sf tf] cf]]. pose g t := choose (fun u => (Vf f t <o \2c ^c u /\ u <c x)). have gp: forall t, inc t (source f)-> (Vf f t <o \2c ^c (g t) /\ (g t) <c x). move => t /(Vf_target ff); rewrite tf => xx. have [sa _ sc]:= (infinite_card_limit2 paln). move/(oltP sa): (sc _ xx) => /x2 [u /oleSltP aux ux]. by apply choose_pr; exists u. set G:= Lf g (cofinality (\2c ^<c x)) x. have ta: lf_axiom g (cofinality (\2c ^<c x)) x. move => t; rewrite - sf => stf; move: (gp _ stf) => [_]. by move /oclt =>/(oltP0) [_ _]. apply: qc => //; exists G; split. by rewrite /G; hnf; aw;split => //; apply: lf_function. move=> t tx; ex_middle bad. have pb: forall z, inc z (cofinality (\2c ^<c x)) -> Vf G z <o t. move => z zsf; move: (zsf); rewrite - sf => zt. have ow: ordinalp (Vf G z). rewrite /G !LfV//;exact: (OS_cardinal (proj31_1 (proj2 (gp _ zt)))). case: (oleT_el (Os_ordinal ox tx) ow) => // yy; case: bad; ex_tac. have pc: forall z, inc z (cofinality (\2c ^<c x)) -> Vf f z <o \2c ^c t. move => z zc;move: (zc); rewrite - sf => /gp [lt1 _]. move: (pb _ zc); rewrite /G LfV//; move => [] /ocle1 /cpow_M2le. rewrite cpowcr cpowcr => /ocle x6 _; apply:(olt_leT lt1 x6). have bad2: inc (\2c ^c t) (\2c ^<c x). have: (\2c ^c t) <c (\2c ^<c x). rewrite - cpowcr. have ot:= (Os_ordinal ox tx). by apply: x1 ; apply /(ocle2P cx ot); apply /oltP. by move => x3; move: (oclt x3); move/(oltP oy). by move: (cf _ bad2) => [z zc le]; move: (oleNgt le (pc _ zc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)