proposition: Lemma up_ZF1: ZF_axioms1 U inc'.
proof: Proof. split. + by exists emptyset. + apply: up_exten. + move => x _; exists (g (union (fun_image (f x) f))); 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 _; exists (g (fun_image (\Po (f x)) g)); 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 f0 _ _; exists (g (fun_image (Zo (f x) p) f0));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. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)