proposition: Lemma Universe_permutation1 (f:= fun x => Yo (x = \0c) \1c (Yo (x = \1c) \0c x)) (U := fun z: Set => True) (R := fun x y => inc x (f y)) (x0 := \1c) (x1:= \0c): [/\ ZF_axioms1 U R, infiniteA U R, choiceA U R, emptysetU U R = x0 & ( doubletonU U R x1 x1 = x1 /\ forall t, doubletonU U R t t = t -> t = x1 \/ (t = singleton t))].
proof: Proof. have h0:= card1_nz. have ff: forall x, f (f x) = x. rewrite /f => x; case: (equal_or_not x \0c) => xz; first by repeat Ytac0. case: (equal_or_not x \1c) => xo; first by repeat Ytac0. by repeat Ytac0. 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 /f -/card_zero; Ytac0; Ytac0. + by rewrite db /x1 -/(singleton _) -/card_one /f; Ytac0; Ytac0. + move => t; rewrite db -/(singleton _) /f. case: (equal_or_not t \0c) => tz //; first by rewrite tz; left. have hb: (singleton t <> \0c). by move => h; move: (set1_1 t); rewrite h => /in_set0. have hc: (singleton t <> \1c) by move => h; move:(set1_inj h). by Ytac0; Ytac0; right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)