proposition: Lemma sup_range_aleph X: fgraph X -> ordinal_fam X -> nonempty (domain X) -> \osup (range (Lg (domain X) (fun z => \aleph (Vg X z)))) = \aleph (\osup (range X)).
proof: Proof. move => ha hb ned. move /normal_ofs_equiv1: aleph_normal => [_ na]. have Ha: (forall x, inc x (range X) -> \0o <=o x). move => x /(range_gP ha) [i idx ->]; apply:(ole0x (hb _ idx)). have Hb: nonempty (range X). by case: ned => [x xd]; exists (Vg X x); apply: inc_V_range. rewrite - (na (range X) Ha Hb);congr union; rewrite Lg_range. set_extens t. move=>/funI_P [z zdf ->]; apply/funI_P; exists (Vg X z) => //. by apply: inc_V_range. by move=>/funI_P [z /(range_gP ha) [s sa ->] ->]; apply:funI_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)