proposition: Theorem disjointU_pr f (h := fun i => Lf P ((Vg f i) *s1 i) (unionb f)) (g := common_ext (disjointU_fam f) h (unionb f)): [/\ source g = disjointU f, target g = unionb f, surjection g & (mutually_disjoint f -> bijection g)].
proof: Proof. set aux:= (Lg (domain f) (fun i => (Vg f i) *s1 i)). have pf:= (partition_disjointU f). have da: (domain aux = domain f) by rewrite /aux; aw. have tap: forall i, inc i (domain aux) -> lf_axiom P ((Vg f i) *s1 i)(unionb f). by move => i id x; move/setX_P=> [_ pv Qi]; union_tac; ue. have fpi: (forall i, inc i (domain aux) -> function_prop (h i) (Vg aux i)(unionb f)). move=> i id; split. + by apply: lf_function;apply: tap. + rewrite lf_source LgV //; ue. + by rewrite lf_target. move:(extension_partition1 pf fpi). rewrite -/g; move => [fpg aag]. move: aag; aw; rewrite/disjointU_fam; aw => aag. have [fg sg tg] := fpg. have sug: (surjection g). apply: surjective_pr5=>//; rewrite /related tg sg. move=> y; move /setUb_P=> [z zdf yg]. set (t:= J y z). have tsg: inc t (disjointU f) by rewrite /t; apply: disjointU_pi. have ps: inc t ((Vg f z) *s1 z) by rewrite /t/indexed ; aww. exists t => //. suff: y = Vf g t by move=>->; apply: Vf_pr3 =>//; rewrite sg. move: (proj33 (aag _ zdf)); rewrite LgV // => sv. by rewrite (sv _ ps) LfV //; [ rewrite/t;aw | by apply: tap; ue]. split=>//. move=> mf; split=>//; split => //. rewrite sg => x y xsg ysg. have [qxd pV xp]:= (disjointU_hi xsg). have [qyd pyV yp] := (disjointU_hi ysg). move: (aag _ qxd); rewrite (LgV qxd) => - [ _ _ ax]. move: (aag _ qyd). rewrite (LgV qyd) => - [ _ _ ay]. have xs: inc x ((Vg f (Q x)) *s1 (Q x)) by apply: setX_i; fprops. have ys: inc y ((Vg f (Q y)) *s1 (Q y)) by apply: setX_i; fprops. rewrite (ax _ xs) (ay _ ys). have ax2: lf_axiom P (Vg f (Q x) *s1 Q x) (unionb f). apply: tap; ue. have ax3: lf_axiom P (Vg f (Q y) *s1 Q y) (unionb f). apply: tap; ue. rewrite !LfV => // sp. move: (mf _ _ qxd qyd); case => sa; first by apply: pair_exten. by empty_tac1 (P x); rewrite sp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)