proposition: Lemma model_union: ZF_axioms1 -> forall a b, U a -> U b -> ( (forall z, U z -> (R z (unionU2 a b) <-> R z a \/ R z b))) /\ (forall z, U z -> (R z (intersectionU2 a b) <-> R z a /\ R z b)).
proof: Proof. move => ax a b ua ub. move: (model_existence ax) => [ea una pa ca ra]. rewrite /unionU2 /intersectionU2. move: (model_existence2 ax ua ub) => []; set c := (doubletonU a b) => cu cp. split. move => z uz; move: (una c cu) => [u1 u2]; split. by move /(u2 _ uz) => [t [tu /(cp _ tu)]]; case => ->; [left| right]. case => zx; apply /(u2 _ uz); [exists a | exists b];split => //. by apply/ (cp _ ua); left. by apply/ (cp _ ub); right. move=> z uz. move: (ca a (fun z => R z b) ua) => []; set d := (setofU _ _) => [du]. by apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)