proposition: Lemma model_existence: ZF_axioms1 -> [/\ emptysetA_pr (emptysetU), forall x, U x -> unionA_pr x (unionU x), forall x, U x -> powersetA_pr x (powersetU x), forall x r, U x -> comprehensionA_pr x r (setofU x r) & forall x (p: property) f, U x -> (forall t, U t -> R t x -> p t -> U (f t)) -> replacementA_pr x p f (funimageU x p f)].
proof: Proof. move => [[x0 ux0] ea ua pa ra]. move: (model_replacement_comprehension ra) => ca. have p1: emptysetA_pr (emptysetU). apply: choose_pr. move :(ca x0 (fun t => ~(R t x0)) ux0) => [c [c1 c2]]. by exists c; split => // t ut; move /(c2 _ ut) => []. have p2: forall x, U x -> unionA_pr x (unionU x). move => x /ua; apply: choose_pr. have p3: forall x, U x -> powersetA_pr x (powersetU x). move => x /pa; apply: choose_pr. have p4: forall x r, U x -> comprehensionA_pr x r (setofU x r). move => x r /ca => h; apply: choose_pr; apply: h. have p5: forall x (p: property) f, U x -> (forall t, U t -> R t x -> p t -> U (f t)) -> replacementA_pr x p f (funimageU x p f). move => x p f ux hf; apply: choose_pr; exact: (ra _ _ _ ux hf). done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)