proposition: Theorem cardinal_supremum2 x: fgraph x -> cardinal_fam x -> exists!b, [/\ cardinalp b, (forall a, inc a (domain x) ->(Vg x a) <=c b) & (forall c, cardinalp c -> (forall a, inc a (domain x) -> (Vg x a) <=c c) -> b <=c c)].
proof: Proof. move=> fg alx. have aly: cardinal_set (range x). by move=> a /(range_gP fg) [z zd ->]; apply: alx. move /unique_existence: (cardinal_supremum1 aly) => [[b [cb bp1 bp2]] _]. apply /unique_existence;split. exists b; split =>//. move=> a adx; apply: bp1; by apply: inc_V_range. move=> c cc hc; apply: bp2=> //. move=> a => /(range_gP fg) [d dd ->]. by apply: hc. move=> u v [cu up1 up2][cv vp1 vp2]. exact:(cleA (up2 _ cv vp1) (vp2 _ cu up1)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)