proposition: Lemma infinite_increasing_power3 X b: ofg_Mle_leo X -> domain X = omega_fct b -> ordinalp b -> limit_ordinal (\osup (range X)) -> cprod (Lg (domain X) (fun z => \aleph (Vg X z))) = \aleph (\osup (range X)) ^c \aleph b.
proof: Proof. move => si dx ob lb. move: (si) => [fgf oob incx]. apply: cleA. have ->: omega_fct b = cardinal (domain X). by rewrite dx card_card //; apply: CS_aleph. by apply: infinite_increasing_power_bound1. set a := (\osup (range X)). set E := (functions (omega_fct b) (omega_fct (union (range X)))). set F := (functions (omega_fct b) (omega_fct b)). set F1 := (injections (omega_fct b) (omega_fct b)). pose G g := Lg (omega_fct b) (fun z => osucc (omega_fct (Vg X(Vf g z)))). have pa: forall f, inc f E -> exists2 g, inc g F1 & inc (graph f) (productb (G g)). move => f fe; move: (cofinality_pr7 si dx ob lb fe) => [g ge h]. move: fe => /functionsP [ff sf tf]. have pa: fgraph (G g) by rewrite /G; fprops. exists g => //; apply /setXb_P => //. rewrite /G; aw;split => //; [ fprops | by rewrite domain_fg | ]. move => i isf; rewrite LgV//. rewrite - sf in isf; move: (h _ isf) => le1. rewrite -/(Vf f i); apply/ oleP => //; exact (proj32 le1). rewrite cpow_pr0. set E1 := gfunctions (omega_fct b) (omega_fct a). have eu: sub E1 (unionb (Lg F1 (fun g => (productb (G g))))). move=> f; rewrite /E1 => fe. move: (gfunctions_hi fe) => [h [fh sh tf gh]]. have hd: inc h E by apply /functionsP;split => //. move: (pa _ hd) => [g ge gv]. by apply /setUb_P; aw; exists g=> //; rewrite LgV//; rewrite -gh. move: (sub_smaller eu). set Y := Lg _ _. have fgy: fgraph Y by rewrite /Y; fprops. move: (csum_pr1 Y) => le1 le2; move: (cleT le2 le1). rewrite {1}/Y; aw ;move => le3; apply: (cleT le3); clear le1 le2 le3. set p := cprod _. have aux: p *c F1 <=c p. have -> : p *c F1 = p *c (cardinal F1) by symmetry; apply: cprod2cr. have ne1: cardinal F1 <> \0c. move/ card_nonempty; apply/nonemptyP. exists (identity (omega_fct b)); apply: Zo_i. apply /functionsP; apply:identity_prop. by move: (identity_fb (omega_fct b)) => []. have s1: sub F1 F by apply: Zo_S. move: (sub_smaller s1); rewrite /F cpow_pr1. move: (CIS_aleph ob) => icb. rewrite (card_card (proj1 icb)) (infinite_power1_b icb) => le2. have le3: \2c ^c omega_fct b <=c p. rewrite - cprod_of_same /cst_graph /p - dx; apply: cprod_increasing; aww. move => x xd; rewrite !LgV//; apply: infinite_ge2; apply: CIS_aleph. apply: (oob _ xd). have le1:= cleT le2 le3. have icp: infinite_c p. move: (cantor (proj1 icb)) => le4. exact (cle_inf_inf icb (cleT (proj1 le4) le3)). rewrite (cprod_inf le1 icp ne1). apply: (cleR (proj1 icp)). suff qa: forall g, inc g F1 -> cardinal (Vg Y g) <=c p. have : csumb F1 (fun a0 => cardinal (Vg Y a0)) <=c csumb F1 (fun _ => p). apply: csum_increasing. fprops. rewrite /cst_graph; fprops. by rewrite /cst_graph; aw. by aw => x xf; rewrite LgV// LgV//; apply: qa. by rewrite csum_of_same => xx; apply: (cleT xx). move => g gi; rewrite /Y LgV//. move: gi => /Zo_P [] /functionsP [fg sg tg] ig. set f:= (Lg (omega_fct b) (fun z : Set => (omega_fct (Vg X (Vf g z))))). have ->: cardinal (productb (G g)) = cprod f. apply:Eqc_setXb. rewrite /G/f; split;aww; move => x xd; rewrite !LgV //. have wi: inc (Vf g x) (domain X). rewrite dx -tg; apply: Vf_target => //; ue. move /card_eqP: (proj2 (CIS_aleph (oob _ wi))). done. rewrite /p. set h := Lg _ _. move: (Imf_Starget fg) => sd1. move: (sd1); rewrite tg - dx => sd. have sd2: sub (Imf g) (domain h) by rewrite /h; aw. have ca: cardinal_fam h. rewrite /h/cardinal_fam; red;aw => i idx; rewrite LgV//. apply: CS_aleph; exact (oob _ idx). have -> : cprod f = cprod (restr h (Imf g)). have fgh: fgraph h by rewrite /h; fprops. rewrite /f /h. move: (restriction_to_image_fb ig) => bg. set Z:= restr _ _. have fgz: fgraph Z by rewrite /Z/restr; apply: restr_fgraph. have trt: target (restriction_to_image g) = domain Z. by rewrite /restriction_to_image /restriction2 /Z restr_d //; aw. rewrite (cprod_Cn trt bg) /composef (domain_fg (proj1 (proj1 bg))). rewrite {1} /restriction_to_image /restriction2; aw; rewrite sg. apply: f_equal; apply: Lg_exten => x xd. have xsd: inc x (source g) by ue. have wi: inc (Vf g x) (Imf g). apply /(Imf_P fg); ex_tac. have ra: restriction2_axioms g (source g) (Imf g) by split. rewrite -/(Vf (restriction_to_image g) x) /restriction_to_image /Z. by rewrite restriction2_V //restr_ev // LgV//; apply: sd. rewrite /h; apply: (cprod_increasing1 _ sd2). rewrite /h;hnf; aw; move => x xd /=; rewrite LgV//;apply: aleph_nz; exact (oob _ xd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)