proposition: Lemma increasing_sup_limit4 X (Y:= Lg (domain X) (fun z => \aleph (Vg X z))) (a := \osup (range X)): ofg_Mlt_lto X -> limit_ordinal (domain X) -> [/\ limit_ordinal a, sub (range X) a & \csup (range Y) = \aleph a].
proof: Proof. move => pa lb. have [xa xb xc] := pa. have osX:= (ofg_Mle_leo_os xa xb). move: (increasing_sup_limit2 pa lb); rewrite -/a => la. split. - exact. - move => t /(range_gP xa) [z sd ->]. have [qa qb] := (ofg_Mlt_lto_p1 xa xc lb sd). have qc: Vg X (osucc z) <=o a. by apply: ord_sup_ub => //; apply /(range_gP xa); ex_tac. apply /(oltP (proj31 la)); split. by apply: (ord_sup_ub osX) ; apply /(range_gP xa); exists z. by move => bad;case:(oltNge qb); rewrite bad. apply:(sup_range_aleph xa xb); exists \0c; exact (proj32 lb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)