proposition: Lemma cpow_less_ec_pr5 x y: infinite_c y -> \2c <=c x -> ~ (exists a, cpow_less_ec_prop x y a) -> exists X, let Y := Lg (domain X) (fun z => x ^c (Vg X z)) in [/\ domain X = \cf y, (forall i, inc i (domain X) -> Vg X i <c y), (forall i, inc i (domain X) -> Vg Y i <c x ^<c y), (y <> omega0 -> card_nz_fam X) & \csup (range Y) = x ^<c y ].
proof: Proof. move => icy x2 ha. move: (ord_index_pr1 icy); set c := ord_index y; move => [oc yv]. case: (equal_or_not c \0c)=> cz. have yo: y = omega0 by rewrite -yv cz aleph0E. have oic:=CIS_omega. case: (finite_or_infinite (proj32 x2)) => fcx; last first. case: ha; rewrite yo;exists \1c; split; first by apply /clt_omegaP; fprops. move => b b1 bo. have bnz: b <> \0c by move/cge1P:b1 => [_ /nesym]. by rewrite(cpowx1 (proj1 fcx)) (cpow_inf fcx) //;apply /clt_omegaP. exists (Lg y id); simpl; rewrite yo; split => //. - by aw; rewrite (proj2 (regular_omega)). - by hnf;aw;move => a ay; rewrite LgV//; apply/clt_omegaP. - aw => i ib; rewrite !LgV//; rewrite (cpow_less_pr5c x2 fcx). by apply/clt_omegaP; fprops. - aw; rewrite /cpow_less Lg_range; congr union. set_extens t;move /funI_P => [z zo ->]; apply/funI_P. exists z; first by apply/(cardinals_ltP CS_omega); apply/clt_omegaP. by rewrite LgV. move /(cardinals_ltP CS_omega): zo => /clt_omegaP zb; exists z => //. by erewrite LgV. case: (ordinal_limA oc) => // lc. move: lc => [d od dv]; case: ha; exists (\aleph d). have ipy := (CIS_aleph od). move: (cnext_pr1 (proj1 ipy)) => [pb pc pd]. move: (cnextE od); rewrite -dv yv => <-; split => //. by move => b l1 /(cnext_pr4 (proj1 ipy)) pe; rewrite (cleA l1 pe). have xnz:= (card_ge2_nz x2). have pa: forall a, a <c y -> exists b, [/\ a <c b, b <c y & x ^c a <c x^c b]. move => a ay; ex_middle bad; case: ha; exists a; split => //. move => b ab lby; ex_middle ne. case: bad; exists b; split => //; split => //; first by dneg eq0; rewrite eq0. exact: (cpow_Meqle xnz ab). have cfy:= (regular_initial_limit1 lc). move: (cofinality_pr4 (proj31 lc)); rewrite - cfy yv; move=> [f fa qe]. move: fa; set cy := \cf y; move => [[[ff sf tf]] cff [_ nf nf1]]. set X := Lg cy (fun z => \aleph (Vf f z)). have fap: forall z, inc z cy -> inc (Vf f z) c. by move => z zx; rewrite -tf; Wtac. have faq: forall z, inc z cy -> ordinalp (Vf f z). move=> z zx; exact: (Os_ordinal oc (fap _ zx)). have pb: cardinal_fam X. by rewrite /X;hnf;aw; move => a ay; rewrite LgV//;apply: CS_aleph; apply: faq. have pc: fg_Mlt_ltc X. hnf; rewrite /X Lgd;move => a b ac bc ab; rewrite !LgV//;apply: aleph_lt_ltc. by apply: nf. have pb': fgraph X by rewrite /X; fprops. have pd: cardinal_set (range X). by move => t /(range_gP pb') [z zd ->]; apply: pb. have pe: \osup (range X) = y. set S := \osup (range X); move: (proj1 icy) => ccy. case: (cleT_el ccy (CS_sup pd)) => pr1. apply:cleA => //; apply: card_ub_sup=> // i /(range_gP pb'). rewrite /X; aw; move => [z zy ->]; rewrite LgV//; move /(oltP oc): (fap _ zy) => []. by rewrite - yv => /aleph_le_lec. have [ra rb rc]: limit_ordinal cy. apply: infinite_card_limit2. by rewrite /cy - yv cfy; apply: cofinality_infinite_limit. have: infinite_c S. have: inc (\aleph (Vf f \0c)) (range X). by apply /(range_gP pb'); rewrite /X; aw; ex_tac; rewrite LgV. move /(card_sup_ub pd); apply: cle_inf_inf; apply: CIS_aleph. by apply: faq. move/ord_index_pr1 => []; set s := ord_index S => os sv. move: pr1; rewrite - /S - sv - yv; move /(aleph_ltc_lt os oc). move: lc => [_ c0 cl]; move => /(oltP oc) /cl /cff [z zc h]. have: inc (\aleph (Vf f z)) (range X). by apply /(range_gP pb'); rewrite /X; aw; ex_tac; rewrite LgV. move/(card_sup_ub pd); rewrite -/S - sv; move /(aleph_lec_le(proj32 h) os). by move /oltSleP => /(oleNgt h). have pi : card_nz_fam X. by rewrite /X; hnf; aw; move => i idx; rewrite LgV//; apply: aleph_nz; apply: faq. have ph: (forall i, inc i (domain X) -> Vg X i <c y). rewrite /X; aw; move => i ic;rewrite LgV//; rewrite -yv. apply: aleph_lt_ltc; move: (fap _ ic). by move /(oltP oc). set Y := (Lg (domain X) (fun z => x ^c (Vg X z))). have pf: forall i, inc i (domain X) -> Vg Y i <c x ^<c y. move => i idx; rewrite /Y LgV//. move: (ph _ idx) => /pa [b [ba /(cpow_less_pr2 x) bb bc]]. exact:(clt_leT bc bb). have pg: union (range Y) = x ^<c y. have rb: fgraph Y by rewrite /Y;fprops. have ra:cardinal_set (range Y). move => t/ (range_gP rb); rewrite /Y; aw; move => [u ud ->]; rewrite LgV//; fprops. have rc: cardinalp (x ^<c y) by apply: CS_cpow_less. have rd: cardinalp (union (range Y)) by apply: CS_sup. move: (@cpow_less_pr0 x y) => re. apply: cleA. apply: card_ub_sup => // i /(range_gP rb). by move=> [z]; rewrite {1}/ Y; aw => /pf [] h _ ->. apply: card_ub_sup => // i /funI_P [z]. move /(cardinals_ltP (proj1 icy)) => rf ->. have [t tr xt]: exists2 t, inc t (range X) & z <=c t. ex_middle bad; case:(cltNge rf). have ccz := proj31_1 rf. rewrite -pe; apply : card_ub_sup => //. move => j jr; case: (cleT_ee (pd _ jr) (proj31_1 rf)) => //. move => zj; case: bad; ex_tac. apply: (cleT (cpow_Meqle xnz xt)). have fgx:fgraph X by rewrite /X; fprops. move: tr => /(range_gP fgx) [v va ->]. apply: card_sup_ub => //; apply /(range_gP rb); aw. by rewrite /Y; aw; ex_tac; rewrite LgV. by exists X; split => //; rewrite /X; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)