proposition: Lemma aleph_sum_pr6 X (Y:= Lg (domain X) (fun z => \aleph (Vg X z))) (a := \osup (range X)): ofg_Mlt_lto X -> limit_ordinal (domain X) -> \aleph a = csum Y.
proof: Proof. move => pa pb. move: (increasing_sup_limit4 pa pb); rewrite -/a; move => [pc pd pe]. rewrite (aleph_sum_pr4 pc pd (refl_equal a)). have [fgx ox si] := pa. have os: ordinal_set (domain X). move => u ub; move: pb => [ob _ _]; exact: (Os_ordinal ob ub). apply:csum_Cn2; split => //. + move => t tx; apply /(range_gP fgx); ex_tac. + move=> u v ud vd sv. case: (oleT_ell (os _ ud) (os _ vd)) => // lt. - by case: (si _ _ ud vd lt). - by case: (si _ _ vd ud lt); rewrite sv. + move => y /(range_gP fgx) [x xd eq]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)