proposition: Lemma model_existence2 : ZF_axioms1 -> forall a b, U a -> U b -> pairA_pr a b (doubletonU a b).
proof: Proof. move => ax a b ua ub. move: (model_existence ax) => [ea una pa ca ra]. move: ax => [es eaa uaa paa raa]. move: ea => []; set e := emptysetU => [ea1 ea2]. move: (pa _ ea1) => []; set e1 := (powersetU e) => [eb1 eb2]. have qa: R e e1 by apply /(eb2 _ ea1). have qb: forall x, U x -> (R x e1 <-> x = e). move => x xu; split; last by move ->. move /(eb2 _ xu) => te; apply:(eaa _ _ xu ea1) => s us; split. apply: (te _ us). by move => v; case: (ea2 _ us). have ee1: e1 <> e. by move => ee1; move /(qb _ eb1): (ee1); rewrite ee1; apply: ea2. move: (pa _ eb1) => []; set e2 := (powersetU e1) => [ec1 ec2]. have qc: R e e2 by apply /(ec2 _ ea1) => t ut ba; case: (ea2 _ ut). have qd: R e1 e2 by apply /(ec2 _ eb1). have qe: forall x, U x -> (R x e2 <-> x = e \/ x = e1). move => x Ux; split; last by case => ->;[ apply qc | apply: qd]. move => xe2; move/ (ec2 _ Ux): xe2 => sa. case: (equal_or_not x e) => xne; [by left | right]. apply: (eaa _ _ Ux eb1) => z uz; split; first by apply: sa. move /(qb _ uz) => ->. case: (p_or_not_p (exists2 t, U t & R t x)). by move => [t ut tx]; move /(sa _ ut): (tx) => /(qb _ ut) => <-. move => ne; case: xne; apply: (eaa _ _ Ux ea1) => s su; split. by move => sx; case: ne; exists s. by move => sz; case: (ea2 _ su). pose f := variant e a b. have fa: f e = a by rewrite /f /variant; Ytac0. have fb: f e1 = b by rewrite /f /variant; Ytac0. have fp: (forall t, U t -> R t e2 -> True -> U (f t)). by move => t _ _ _; rewrite /f /variant;Ytac h. move: (ra e2 (fun _ => True) f ec1 fp)=> []. set c := funimageU _ _ _ => [c1 c2]. apply: choose_pr; exists c;split => // t ut; split. move/(c2 _ ut) => [s us [/(qe _ us) rs2 _ ->]]. by case: rs2 => ->; [ left | right]. case => ->. by apply /(c2 _ ua); exists e. by apply /(c2 _ ub); exists e1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)