proposition: Lemma AC_variants: let AC:= forall x, (forall z, inc z x -> nonempty z) -> (forall z z', inc z x -> inc z' x -> z = z' \/ disjoint z z') -> (exists y, forall z, inc z x -> singletonp (y \cap z)) in (AC -> (forall f, nonempty_fam f -> nonempty (productb f))) /\ (AC -> forall x, exists y, [/\ fgraph y, domain y = \Po x -s1 emptyset & forall z, sub z x -> nonempty z -> inc (Vg y z) z]) /\ ((forall x, exists r, forall z, inc z x -> nonempty z -> inc (r z) z) -> AC).
proof: Proof. move => AC. have pr1: AC -> (forall f, nonempty_fam f -> nonempty (productb f)). move => ac f nef. set d := domain f. set x := fun_image d (fun z => (singleton z) \times (Vg f z)). have pa: (forall z, inc z x -> nonempty z). move => z /funI_P [u /nef [v ud] ->];exists (J u v); apply: setXp_i; fprops. have pb: (forall z z', inc z x -> inc z' x -> z = z' \/ disjoint z z'). move => z z' /funI_P [u /nef _ ->] /funI_P [v /nef _ ->]. case: (equal_or_not u v); first by move => ->; left. move => uv; right; apply: disjoint_pr => w /setX_P [_ /set1_P pw _]. by move => /setX_P [_ /set1_P pw' _]; case: uv; rewrite -pw -pw'. move: (ac _ pa pb) => [y yp]. set y1:= y \cap (union x). have yp': forall z, inc z x -> singletonp (y1 \cap z). move => z zx; move/yp: (zx) => [t t1];exists t; apply: set1_pr. move: (set1_1 t); rewrite -t1 => /setI2_P [ty tz]; apply /setI2_P. split => //; apply /setI2_P; split => //; union_tac. move => u /setI2_P [/setI2_P [p1 p2] p3]. by apply /set1_P; rewrite -t1; apply /setI2_P. have pc: forall s, inc s y1 -> exists2 b, inc b d & let a:= singleton b \times Vg f b in [/\ inc a x, y1 \cap a = singleton s & inc s (singleton b \times Vg f b)]. move => s sy1; move: (sy1) => /setI2_P [_ /setU_P [a sa sb]]. have pc:inc s (y1 \cap a) by apply /setI2_P. move /funI_P: (sb) => [b ba bb]; ex_tac; rewrite -bb; split => //. apply: set1_pr1; first by exists s. by move => z za; move:(yp' _ sb) => /singletonP [_ ss]; apply ss. have sy1: fgraph y1. split; first by move => t /pc [b _ [_ _ /setX_P []]]. move => s s' s1 s2 sp. move: (pc _ s1)(pc _ s2) => [a ax [i1a i2a i3a]] [b bx [i1b i2b i3b]]. move: i3a i3b => /setX_P [_ /set1_P psa _] /setX_P [_ /set1_P psb _]. by apply: set1_inj; rewrite -i2a -i2b - psa sp psb. have dy1: domain y1 = domain f. set_extens t. by move /funI_P => [z /pc [b bd [_ _ /setX_P [_ /set1_P -> _]]]-> ]. move => tdf. set z := (singleton t \times Vg f t). have zx: inc z x by apply /funI_P;ex_tac. move: (yp' _ zx) => [a sa]. have ay1: inc a y1 by move: (set1_1 a); rewrite - sa => /setI2_P []. have : inc a z by move: (set1_1 a); rewrite - sa => /setI2_P []. move => /setX_P [_ /set1_P pat _]. apply /funI_P; by ex_tac. exists y1; apply /setXb_P; split => //. move => i idf. set z := (singleton i \times Vg f i). have zx: inc z x by apply /funI_P;ex_tac. move: (yp' _ zx) => [a sa]. have ay1: inc a y1 by move: (set1_1 a); rewrite - sa => /setI2_P []. move: (pc _ ay1) => [b b1 [b2 b3 b4]]. have : inc a z by move: (set1_1 a); rewrite - sa => /setI2_P []. move => /setX_P [_ /set1_P pat _]. move: (set1_1 a); rewrite -b3 => /setI2_P [_ /setX_P [_ /set1_P sb sc]]. by rewrite - pat - (pr2_V sy1 ay1) sb. have pr2: (AC -> forall x, exists y, [/\ fgraph y, domain y = \Po x -s1 emptyset & forall z, sub z x -> nonempty z -> inc (Vg y z) z]). move => ac x; set f := Lg (\Po x -s1 emptyset) id. have : nonempty_fam f. by rewrite /f;hnf; aw;move => t tp; rewrite LgV//; move /setC1_P: tp => [_ /nonemptyP]. move /(pr1 ac) => [y /setXb_P [pa pb pc]]; exists y; split => //. by rewrite pb /f;aw. move => z zb zne. have zi: inc z (\Po x -s1 emptyset). apply /setC1_P; split => //; [by apply/setP_P | by apply /nonemptyP]. have: inc z (domain f) by rewrite /f; aw. move /pc;rewrite /f LgV//. have pr3: (forall x : Set, exists r : Set -> Set, forall z : Set, inc z x -> nonempty z -> inc (r z) z) -> AC. move => h x x1 x2; move: (h x) => [r ra]. set y := fun_image x r; exists y => z zx. have p1: inc (r z) z by apply: ra => //; apply: x1. have p2: inc (r z) y by apply /funI_P;ex_tac. apply/singletonP; split; first by exists (r z); apply/ setI2_P. move => a b /setI2_P [/funI_P [u ua ub] az] /setI2_P [/funI_P [v va vb] bz]. move: (ra _ ua (x1 _ ua)) (ra _ va (x1 _ va)) => uc vc. move: (x2 _ _ zx ua); case => zu; last by empty_tac1 a; ue. move: (x2 _ _ zx va); case => zv; last by empty_tac1 b; ue. by rewrite ub vb - zu -zv. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)