proposition: Lemma Universe_permutation2 (U := fun z: Set => True) (R := fun x y => inc x (f y)) (x1 := \1c) (x0:= \0c): [/\ ZF_axioms1 U R, infiniteA U R, choiceA U R, emptysetU U R = x0 & ((forall x, inc x Nat -> x <> \0c -> doubletonU U R x x = x) /\ forall t, doubletonU U R t t = t -> (inc t Nat /\ t <> \0c) \/ singleton t = t)].
proof: Proof. have h0:= card1_nz. have ff:= up2_fperm. move: (up_values ff ff) => [us _ _ _ [_ db]]. split; last split. + exact: (up_ZF1 ff ff). + exact: (up_infinite ff ff). + exact: (up_choice ff ff). + by rewrite us up2_f0. + by move => x xb xnz; rewrite db up2_fnats. + move => t; rewrite db -/(singleton _) => sft. move:(f_equal f sft); rewrite up2_fperm => sft1. case: (equal_or_not t \0c) => tb. by move: sft1; rewrite tb up2_f0=> h; case: C1_ne_C0. case: (inc_or_not t Nat) => itb; first by left. have hb: ~ (inc t Nat /\ t <> \0c) by move => []. move:sft1; rewrite /f /universe_permutation_fun; Ytac0. Ytac hh; last by right. move: hh => [y [yb ynz tv]]; rewrite {2} tv setU_1 => hha. have ha: inc t y by rewrite - hha; fprops. have hc: inc y t by rewrite tv; fprops. case: (ordinal_irreflexive (OS_nat yb)). exact: (ordinal_transitive (OS_nat yb) ha hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)