proposition: Lemma infinite_increasing_power4 X (Y:= Lg (domain X)(fun z => \aleph (Vg X z))) (a := \osup (range X)): ofg_Mlt_lto X -> limit_ordinal (domain X) -> (cardinal (domain X) <=c \aleph a /\ \aleph a <c (cprod Y)).
proof: Proof. move => pa pb. move: (increasing_sup_limit4 pa pb);rewrite -/Y -/a; move => [pc pd pe]. move: pa => [fgx xo xi]. move: (pc)(pb) => [oa _ _] [odx _ ldx]. have pa: cardinal (domain X) <=c (cardinal a). have:bijection (Lf (Vg X) (domain X) (range X)). apply: lf_bijective. move => t td; apply /(range_gP fgx); ex_tac. move => u v ud vd sv. case: (oleT_ell (Os_ordinal odx ud)(Os_ordinal odx vd)) => // cuv. by move: (xi _ _ ud vd cuv); rewrite sv;move => [_]. by move: (xi _ _ vd ud cuv); rewrite sv;move => [_]. move => y /(range_gP fgx) [x xd ->]; ex_tac. move/card_bijection; aw => ->; apply: (sub_smaller pd). move: (ocle1 (aleph_pr6 oa)); rewrite (card_card (CS_aleph oa)) => lt1. move: (cleT pa lt1) => le1 {pa lt1}. split; first by exact. have ia:=(CIS_aleph (proj31 pc)). have cfy: cardinal_fam Y. rewrite /Y;hnf;aw; move => i idx; rewrite LgV//; apply: CS_aleph;fprops. have fgY: fgraph Y by rewrite /Y; fprops. have cd1: cardinal (domain Y) <=c \aleph a by rewrite /Y; aw. have <-: csum Y = \aleph a. by rewrite /Y - pe; apply: csum_of_small_b4 => //; rewrite pe. set Z := Lg (domain X) (fun z => (\aleph (Vg X (osucc z)))). have fgZ: fgraph Z by rewrite /Z; fprops. have sd: domain Y = domain Z by rewrite /Y /Z; aw. have inc1: (forall i, inc i (domain Y) -> Vg Y i <c Vg Z i). rewrite /Y/Z; aw; move => i idx; rewrite !LgV//; apply: aleph_lt_ltc. apply: xi => //; [ by apply: ldx | apply: (oltS (Os_ordinal odx idx)) ]. apply: (clt_leT (compare_sum_prod fgY fgZ sd inc1)). set X1 := fun_image (domain X) osucc. have scx1: sub X1 (domain X) by move =>t /funI_P [z zd ->]; apply: ldx. have <-: cprod (restr Y X1) = cprod Z. have ->: cprod (restr Y X1) = cprodb X1 (fun z => \omega (Vg X z)). by apply:cprodb_exten => i ii; rewrite /Y; aw; rewrite LgV//; apply: scx1. rewrite /Z -/(cprodb _ _); apply:cprod_Cn2; split. + move => t td; apply /funI_P; ex_tac. + move => u v ud vd. exact: (osucc_inj (Os_ordinal odx ud)(Os_ordinal odx vd)). + by move => y /funI_P. apply: cprod_increasing1 => //; last by rewrite /Y; aw. by hnf;rewrite /Y; aw;move => x xd; rewrite LgV//; apply: aleph_nz; apply: xo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)