Metamath Proof Explorer

Theorem dfac5

Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Theorem 6M(4) of Enderton p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC. (Contributed by NM, 11-Apr-2004) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dfac5 ⊢ CHOICE ↔ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y

Proof

Step Hyp Ref Expression
1 dfac4 ⊢ CHOICE ↔ ∀ x ∃ f f Fn x ∧ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w
2 neeq1 ⊢ z = w → z ≠ ∅ ↔ w ≠ ∅
3 2 cbvralvw ⊢ ∀ z ∈ x z ≠ ∅ ↔ ∀ w ∈ x w ≠ ∅
4 3 anbi2i ⊢ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ ∀ z ∈ x z ≠ ∅ ↔ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ ∀ w ∈ x w ≠ ∅
5 r19.26 ⊢ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ w ≠ ∅ ↔ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ ∀ w ∈ x w ≠ ∅
6 4 5 bitr4i ⊢ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ ∀ z ∈ x z ≠ ∅ ↔ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ w ≠ ∅
7 pm3.35 ⊢ w ≠ ∅ ∧ w ≠ ∅ → f ⁡ w ∈ w → f ⁡ w ∈ w
8 7 ancoms ⊢ w ≠ ∅ → f ⁡ w ∈ w ∧ w ≠ ∅ → f ⁡ w ∈ w
9 8 ralimi ⊢ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ w ≠ ∅ → ∀ w ∈ x f ⁡ w ∈ w
10 6 9 sylbi ⊢ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ ∀ z ∈ x z ≠ ∅ → ∀ w ∈ x f ⁡ w ∈ w
11 r19.26 ⊢ ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ ↔ ∀ w ∈ x f ⁡ w ∈ w ∧ ∀ w ∈ x z ≠ w → z ∩ w = ∅
12 elin ⊢ v ∈ z ∩ ran ⁡ f ↔ v ∈ z ∧ v ∈ ran ⁡ f
13 fvelrnb ⊢ f Fn x → v ∈ ran ⁡ f ↔ ∃ t ∈ x f ⁡ t = v
14 13 biimpac ⊢ v ∈ ran ⁡ f ∧ f Fn x → ∃ t ∈ x f ⁡ t = v
15 fveq2 ⊢ w = t → f ⁡ w = f ⁡ t
16 id ⊢ w = t → w = t
17 15 16 eleq12d ⊢ w = t → f ⁡ w ∈ w ↔ f ⁡ t ∈ t
18 neeq2 ⊢ w = t → z ≠ w ↔ z ≠ t
19 ineq2 ⊢ w = t → z ∩ w = z ∩ t
20 19 eqeq1d ⊢ w = t → z ∩ w = ∅ ↔ z ∩ t = ∅
21 18 20 imbi12d ⊢ w = t → z ≠ w → z ∩ w = ∅ ↔ z ≠ t → z ∩ t = ∅
22 17 21 anbi12d ⊢ w = t → f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ ↔ f ⁡ t ∈ t ∧ z ≠ t → z ∩ t = ∅
23 22 rspcv ⊢ t ∈ x → ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → f ⁡ t ∈ t ∧ z ≠ t → z ∩ t = ∅
24 minel ⊢ f ⁡ t ∈ t ∧ z ∩ t = ∅ → ¬ f ⁡ t ∈ z
25 24 ex ⊢ f ⁡ t ∈ t → z ∩ t = ∅ → ¬ f ⁡ t ∈ z
26 25 imim2d ⊢ f ⁡ t ∈ t → z ≠ t → z ∩ t = ∅ → z ≠ t → ¬ f ⁡ t ∈ z
27 26 imp ⊢ f ⁡ t ∈ t ∧ z ≠ t → z ∩ t = ∅ → z ≠ t → ¬ f ⁡ t ∈ z
28 27 necon4ad ⊢ f ⁡ t ∈ t ∧ z ≠ t → z ∩ t = ∅ → f ⁡ t ∈ z → z = t
29 eleq1 ⊢ f ⁡ t = v → f ⁡ t ∈ z ↔ v ∈ z
30 29 biimpar ⊢ f ⁡ t = v ∧ v ∈ z → f ⁡ t ∈ z
31 28 30 impel ⊢ f ⁡ t ∈ t ∧ z ≠ t → z ∩ t = ∅ ∧ f ⁡ t = v ∧ v ∈ z → z = t
32 fveq2 ⊢ z = t → f ⁡ z = f ⁡ t
33 eqeq2 ⊢ f ⁡ t = v → f ⁡ z = f ⁡ t ↔ f ⁡ z = v
34 eqcom ⊢ f ⁡ z = v ↔ v = f ⁡ z
35 33 34 syl6bb ⊢ f ⁡ t = v → f ⁡ z = f ⁡ t ↔ v = f ⁡ z
36 32 35 syl5ib ⊢ f ⁡ t = v → z = t → v = f ⁡ z
37 36 ad2antrl ⊢ f ⁡ t ∈ t ∧ z ≠ t → z ∩ t = ∅ ∧ f ⁡ t = v ∧ v ∈ z → z = t → v = f ⁡ z
38 31 37 mpd ⊢ f ⁡ t ∈ t ∧ z ≠ t → z ∩ t = ∅ ∧ f ⁡ t = v ∧ v ∈ z → v = f ⁡ z
39 38 exp32 ⊢ f ⁡ t ∈ t ∧ z ≠ t → z ∩ t = ∅ → f ⁡ t = v → v ∈ z → v = f ⁡ z
40 23 39 syl6com ⊢ ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → t ∈ x → f ⁡ t = v → v ∈ z → v = f ⁡ z
41 40 com14 ⊢ v ∈ z → t ∈ x → f ⁡ t = v → ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → v = f ⁡ z
42 41 rexlimdv ⊢ v ∈ z → ∃ t ∈ x f ⁡ t = v → ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → v = f ⁡ z
43 14 42 syl5 ⊢ v ∈ z → v ∈ ran ⁡ f ∧ f Fn x → ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → v = f ⁡ z
44 43 expd ⊢ v ∈ z → v ∈ ran ⁡ f → f Fn x → ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → v = f ⁡ z
45 44 com4t ⊢ f Fn x → ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → v ∈ z → v ∈ ran ⁡ f → v = f ⁡ z
46 45 imp4b ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → v ∈ z ∧ v ∈ ran ⁡ f → v = f ⁡ z
47 12 46 syl5bi ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ≠ w → z ∩ w = ∅ → v ∈ z ∩ ran ⁡ f → v = f ⁡ z
48 11 47 sylan2br ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ ∀ w ∈ x z ≠ w → z ∩ w = ∅ → v ∈ z ∩ ran ⁡ f → v = f ⁡ z
49 48 anassrs ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ ∀ w ∈ x z ≠ w → z ∩ w = ∅ → v ∈ z ∩ ran ⁡ f → v = f ⁡ z
50 49 adantlr ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ∈ x ∧ ∀ w ∈ x z ≠ w → z ∩ w = ∅ → v ∈ z ∩ ran ⁡ f → v = f ⁡ z
51 fveq2 ⊢ w = z → f ⁡ w = f ⁡ z
52 id ⊢ w = z → w = z
53 51 52 eleq12d ⊢ w = z → f ⁡ w ∈ w ↔ f ⁡ z ∈ z
54 53 rspcv ⊢ z ∈ x → ∀ w ∈ x f ⁡ w ∈ w → f ⁡ z ∈ z
55 fnfvelrn ⊢ f Fn x ∧ z ∈ x → f ⁡ z ∈ ran ⁡ f
56 55 expcom ⊢ z ∈ x → f Fn x → f ⁡ z ∈ ran ⁡ f
57 54 56 anim12d ⊢ z ∈ x → ∀ w ∈ x f ⁡ w ∈ w ∧ f Fn x → f ⁡ z ∈ z ∧ f ⁡ z ∈ ran ⁡ f
58 elin ⊢ f ⁡ z ∈ z ∩ ran ⁡ f ↔ f ⁡ z ∈ z ∧ f ⁡ z ∈ ran ⁡ f
59 57 58 syl6ibr ⊢ z ∈ x → ∀ w ∈ x f ⁡ w ∈ w ∧ f Fn x → f ⁡ z ∈ z ∩ ran ⁡ f
60 59 expd ⊢ z ∈ x → ∀ w ∈ x f ⁡ w ∈ w → f Fn x → f ⁡ z ∈ z ∩ ran ⁡ f
61 60 com13 ⊢ f Fn x → ∀ w ∈ x f ⁡ w ∈ w → z ∈ x → f ⁡ z ∈ z ∩ ran ⁡ f
62 61 imp31 ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ∈ x → f ⁡ z ∈ z ∩ ran ⁡ f
63 eleq1 ⊢ v = f ⁡ z → v ∈ z ∩ ran ⁡ f ↔ f ⁡ z ∈ z ∩ ran ⁡ f
64 62 63 syl5ibrcom ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ∈ x → v = f ⁡ z → v ∈ z ∩ ran ⁡ f
65 64 adantr ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ∈ x ∧ ∀ w ∈ x z ≠ w → z ∩ w = ∅ → v = f ⁡ z → v ∈ z ∩ ran ⁡ f
66 50 65 impbid ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ∈ x ∧ ∀ w ∈ x z ≠ w → z ∩ w = ∅ → v ∈ z ∩ ran ⁡ f ↔ v = f ⁡ z
67 66 ex ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ∈ x → ∀ w ∈ x z ≠ w → z ∩ w = ∅ → v ∈ z ∩ ran ⁡ f ↔ v = f ⁡ z
68 67 alrimdv ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ∈ x → ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∀ v v ∈ z ∩ ran ⁡ f ↔ v = f ⁡ z
69 fvex ⊢ f ⁡ z ∈ V
70 eqeq2 ⊢ h = f ⁡ z → v = h ↔ v = f ⁡ z
71 70 bibi2d ⊢ h = f ⁡ z → v ∈ z ∩ ran ⁡ f ↔ v = h ↔ v ∈ z ∩ ran ⁡ f ↔ v = f ⁡ z
72 71 albidv ⊢ h = f ⁡ z → ∀ v v ∈ z ∩ ran ⁡ f ↔ v = h ↔ ∀ v v ∈ z ∩ ran ⁡ f ↔ v = f ⁡ z
73 69 72 spcev ⊢ ∀ v v ∈ z ∩ ran ⁡ f ↔ v = f ⁡ z → ∃ h ∀ v v ∈ z ∩ ran ⁡ f ↔ v = h
74 eu6 ⊢ ∃! v v ∈ z ∩ ran ⁡ f ↔ ∃ h ∀ v v ∈ z ∩ ran ⁡ f ↔ v = h
75 73 74 sylibr ⊢ ∀ v v ∈ z ∩ ran ⁡ f ↔ v = f ⁡ z → ∃! v v ∈ z ∩ ran ⁡ f
76 68 75 syl6 ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w ∧ z ∈ x → ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃! v v ∈ z ∩ ran ⁡ f
77 76 ralimdva ⊢ f Fn x ∧ ∀ w ∈ x f ⁡ w ∈ w → ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∀ z ∈ x ∃! v v ∈ z ∩ ran ⁡ f
78 77 ex ⊢ f Fn x → ∀ w ∈ x f ⁡ w ∈ w → ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∀ z ∈ x ∃! v v ∈ z ∩ ran ⁡ f
79 10 78 syl5 ⊢ f Fn x → ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w ∧ ∀ z ∈ x z ≠ ∅ → ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∀ z ∈ x ∃! v v ∈ z ∩ ran ⁡ f
80 79 expd ⊢ f Fn x → ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w → ∀ z ∈ x z ≠ ∅ → ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∀ z ∈ x ∃! v v ∈ z ∩ ran ⁡ f
81 80 imp4b ⊢ f Fn x ∧ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w → ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∀ z ∈ x ∃! v v ∈ z ∩ ran ⁡ f
82 vex ⊢ f ∈ V
83 82 rnex ⊢ ran ⁡ f ∈ V
84 ineq2 ⊢ y = ran ⁡ f → z ∩ y = z ∩ ran ⁡ f
85 84 eleq2d ⊢ y = ran ⁡ f → v ∈ z ∩ y ↔ v ∈ z ∩ ran ⁡ f
86 85 eubidv ⊢ y = ran ⁡ f → ∃! v v ∈ z ∩ y ↔ ∃! v v ∈ z ∩ ran ⁡ f
87 86 ralbidv ⊢ y = ran ⁡ f → ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ z ∈ x ∃! v v ∈ z ∩ ran ⁡ f
88 83 87 spcev ⊢ ∀ z ∈ x ∃! v v ∈ z ∩ ran ⁡ f → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
89 81 88 syl6 ⊢ f Fn x ∧ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w → ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
90 89 exlimiv ⊢ ∃ f f Fn x ∧ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w → ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
91 90 alimi ⊢ ∀ x ∃ f f Fn x ∧ ∀ w ∈ x w ≠ ∅ → f ⁡ w ∈ w → ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
92 1 91 sylbi ⊢ CHOICE → ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
93 eqid ⊢ u | u ≠ ∅ ∧ ∃ t ∈ h u = t × t = u | u ≠ ∅ ∧ ∃ t ∈ h u = t × t
94 eqid ⊢ ⋃ u | u ≠ ∅ ∧ ∃ t ∈ h u = t × t ∩ y = ⋃ u | u ≠ ∅ ∧ ∃ t ∈ h u = t × t ∩ y
95 biid ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
96 93 94 95 dfac5lem5 ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y → ∃ f ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w
97 96 alrimiv ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y → ∀ h ∃ f ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w
98 dfac3 ⊢ CHOICE ↔ ∀ h ∃ f ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w
99 97 98 sylibr ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y → CHOICE
100 92 99 impbii ⊢ CHOICE ↔ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y