proposition: Lemma infinite_increasing_power1 X b: ofg_Mle_leo X -> domain X = \omega b -> ordinalp b -> cprod (Lg (domain X) (fun z => \aleph (Vg X z))) = \aleph (\osup (range X)) ^c \aleph b.
proof: Proof. move => px dx ob. set Y := Lg _ _. have p1: fgraph Y by rewrite /Y; fprops. have dY: domain Y = \aleph b by rewrite /Y Lgd dx. have p2: infinite_c (domain Y) by rewrite dY; apply CIS_aleph. move: px => [fgx pa xi]. have nedx: nonempty (domain X). exists \0c; rewrite dx - dY; apply:(omega_limit3 p2); exact:NS0. have p3: cardinal_pos_fam Y. by rewrite /Y; hnf;aw => a adx; rewrite LgV//; apply: aleph_nz1;apply: pa. have p4: fg_Mle_lec Y. hnf; rewrite /Y; aw => u v ud vd uv; rewrite !LgV//; apply: aleph_le_lec. apply: (xi _ _ ud vd uv). rewrite (infinite_increasing_power p1 p2 p3 p4). by rewrite (sup_range_aleph fgx pa nedx) dY. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)