proposition: Lemma up_values: [/\ emptysetU U inc' = g emptyset, forall x, unionU U inc' x = (g (union (fun_image (f x) f))), forall x, powersetU U inc' x = (g (fun_image (\Po (f x)) g)), forall x p, setofU U inc' x p = (g (Zo (f x) p)) & (forall x p f0, funimageU U inc' x p f0 = (g (fun_image (Zo (f x) p) f0))) /\ (forall x y, doubletonU U inc' x y = g (doubleton x y))].
proof: Proof. move:(model_uniqueness up_exten) => [uU uP uC uR [uE up]]. move:(model_existence up_ZF1) => [eE eU eP eC eR]. split; last split. + by apply: uE => //; split => // t _; rewrite /inc' fg => /in_set0. + move => x; apply:(uU x); first by apply:eU. split => // y _; rewrite /inc' fg; split. move /setU_P => [z yz /funI_P [t zx zv]]; exists t; split => //; ue. move => [z [_ zfx yfz]]; union_tac; apply /funI_P; ex_tac. + move =>x; apply(uP x); first by apply:eP. split => // y _ ;rewrite /inc' fg; split. by move/funI_P=> [z /setP_P h1 ->] t _; rewrite fg => /h1. move => h; apply/funI_P; exists (f y); rewrite ? gf //. by apply/setP_P => t; apply:(h _ (up_Ut t)). + move => x p; apply:(uC x p); first by apply:eC. split => // y _; rewrite /inc' fg; exact:(Zo_P (f x) p y). + move => x p f0; apply:(uR x p f0); first by apply:eR. split => // y _; rewrite /inc' fg; split. move => /funI_P [z /Zo_P [pa pb] pc]; exists z => //. by move => [t _ [pa pb pc]]; apply /funI_P; exists t => //; apply/Zo_P. + move => x y; apply:(up x y). exact:(model_existence2 up_ZF1 (up_Ut x) (up_Ut y)). by split => // t _; rewrite /inc' fg; move:(set2_P t x y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)