proposition: Lemma infinite_increasing_power_bound1 X: fgraph X -> ordinal_fam X -> cprod (Lg (domain X) (fun z => \aleph (Vg X z))) <=c \aleph (\osup (range X)) ^c (cardinal (domain X)).
proof: Proof. move => fX ogx. set Y := Lg _ _. case: (emptyset_dichot (domain X)) => xne. rewrite /Y xne cprod_trivial;aw; trivial. rewrite cardinal_set0 cpowx0; fprops. have <- : \osup (range Y) = \aleph (\osup (range X)). apply:(sup_range_aleph fX ogx xne). have -> : domain X = domain Y by rewrite /Y; aw. apply:infinite_increasing_power_bound0; rewrite/Y; fprops; hnf; aw. move => i idx; rewrite LgV//; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)