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∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y

Proof

Step Hyp Ref Expression
1 dfac4 ⊢CHOICE↔∀x∃ffFnx∧∀w∈xw≠∅→f⁡w∈w
2 neeq1 ⊢z=w→z≠∅↔w≠∅
3 2 cbvralvw ⊢∀z∈xz≠∅↔∀w∈xw≠∅
4 3 anbi2i ⊢∀w∈xw≠∅→f⁡w∈w∧∀z∈xz≠∅↔∀w∈xw≠∅→f⁡w∈w∧∀w∈xw≠∅
5 r19.26 ⊢∀w∈xw≠∅→f⁡w∈w∧w≠∅↔∀w∈xw≠∅→f⁡w∈w∧∀w∈xw≠∅
6 4 5 bitr4i ⊢∀w∈xw≠∅→f⁡w∈w∧∀z∈xz≠∅↔∀w∈xw≠∅→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∈xw≠∅→f⁡w∈w∧w≠∅→∀w∈xf⁡w∈w
10 6 9 sylbi ⊢∀w∈xw≠∅→f⁡w∈w∧∀z∈xz≠∅→∀w∈xf⁡w∈w
11 r19.26 ⊢∀w∈xf⁡w∈w∧z≠w→z∩w=∅↔∀w∈xf⁡w∈w∧∀w∈xz≠w→z∩w=∅
12 elin ⊢v∈z∩ran⁡f↔v∈z∧v∈ran⁡f
13 fvelrnb ⊢fFnx→v∈ran⁡f↔∃t∈xf⁡t=v
14 13 biimpac ⊢v∈ran⁡f∧fFnx→∃t∈xf⁡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∈xf⁡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 bitrdi ⊢f⁡t=v→f⁡z=f⁡t↔v=f⁡z
36 32 35 imbitrid ⊢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∈xf⁡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∈xf⁡w∈w∧z≠w→z∩w=∅→v=f⁡z
42 41 rexlimdv ⊢v∈z→∃t∈xf⁡t=v→∀w∈xf⁡w∈w∧z≠w→z∩w=∅→v=f⁡z
43 14 42 syl5 ⊢v∈z→v∈ran⁡f∧fFnx→∀w∈xf⁡w∈w∧z≠w→z∩w=∅→v=f⁡z
44 43 expd ⊢v∈z→v∈ran⁡f→fFnx→∀w∈xf⁡w∈w∧z≠w→z∩w=∅→v=f⁡z
45 44 com4t ⊢fFnx→∀w∈xf⁡w∈w∧z≠w→z∩w=∅→v∈z→v∈ran⁡f→v=f⁡z
46 45 imp4b ⊢fFnx∧∀w∈xf⁡w∈w∧z≠w→z∩w=∅→v∈z∧v∈ran⁡f→v=f⁡z
47 12 46 biimtrid ⊢fFnx∧∀w∈xf⁡w∈w∧z≠w→z∩w=∅→v∈z∩ran⁡f→v=f⁡z
48 11 47 sylan2br ⊢fFnx∧∀w∈xf⁡w∈w∧∀w∈xz≠w→z∩w=∅→v∈z∩ran⁡f→v=f⁡z
49 48 anassrs ⊢fFnx∧∀w∈xf⁡w∈w∧∀w∈xz≠w→z∩w=∅→v∈z∩ran⁡f→v=f⁡z
50 49 adantlr ⊢fFnx∧∀w∈xf⁡w∈w∧z∈x∧∀w∈xz≠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∈xf⁡w∈w→f⁡z∈z
55 fnfvelrn ⊢fFnx∧z∈x→f⁡z∈ran⁡f
56 55 expcom ⊢z∈x→fFnx→f⁡z∈ran⁡f
57 54 56 anim12d ⊢z∈x→∀w∈xf⁡w∈w∧fFnx→f⁡z∈z∧f⁡z∈ran⁡f
58 elin ⊢f⁡z∈z∩ran⁡f↔f⁡z∈z∧f⁡z∈ran⁡f
59 57 58 imbitrrdi ⊢z∈x→∀w∈xf⁡w∈w∧fFnx→f⁡z∈z∩ran⁡f
60 59 expd ⊢z∈x→∀w∈xf⁡w∈w→fFnx→f⁡z∈z∩ran⁡f
61 60 com13 ⊢fFnx→∀w∈xf⁡w∈w→z∈x→f⁡z∈z∩ran⁡f
62 61 imp31 ⊢fFnx∧∀w∈xf⁡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 ⊢fFnx∧∀w∈xf⁡w∈w∧z∈x→v=f⁡z→v∈z∩ran⁡f
65 64 adantr ⊢fFnx∧∀w∈xf⁡w∈w∧z∈x∧∀w∈xz≠w→z∩w=∅→v=f⁡z→v∈z∩ran⁡f
66 50 65 impbid ⊢fFnx∧∀w∈xf⁡w∈w∧z∈x∧∀w∈xz≠w→z∩w=∅→v∈z∩ran⁡f↔v=f⁡z
67 66 ex ⊢fFnx∧∀w∈xf⁡w∈w∧z∈x→∀w∈xz≠w→z∩w=∅→v∈z∩ran⁡f↔v=f⁡z
68 67 alrimdv ⊢fFnx∧∀w∈xf⁡w∈w∧z∈x→∀w∈xz≠w→z∩w=∅→∀vv∈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→∀vv∈z∩ran⁡f↔v=h↔∀vv∈z∩ran⁡f↔v=f⁡z
73 69 72 spcev ⊢∀vv∈z∩ran⁡f↔v=f⁡z→∃h∀vv∈z∩ran⁡f↔v=h
74 eu6 ⊢∃!vv∈z∩ran⁡f↔∃h∀vv∈z∩ran⁡f↔v=h
75 73 74 sylibr ⊢∀vv∈z∩ran⁡f↔v=f⁡z→∃!vv∈z∩ran⁡f
76 68 75 syl6 ⊢fFnx∧∀w∈xf⁡w∈w∧z∈x→∀w∈xz≠w→z∩w=∅→∃!vv∈z∩ran⁡f
77 76 ralimdva ⊢fFnx∧∀w∈xf⁡w∈w→∀z∈x∀w∈xz≠w→z∩w=∅→∀z∈x∃!vv∈z∩ran⁡f
78 77 ex ⊢fFnx→∀w∈xf⁡w∈w→∀z∈x∀w∈xz≠w→z∩w=∅→∀z∈x∃!vv∈z∩ran⁡f
79 10 78 syl5 ⊢fFnx→∀w∈xw≠∅→f⁡w∈w∧∀z∈xz≠∅→∀z∈x∀w∈xz≠w→z∩w=∅→∀z∈x∃!vv∈z∩ran⁡f
80 79 expd ⊢fFnx→∀w∈xw≠∅→f⁡w∈w→∀z∈xz≠∅→∀z∈x∀w∈xz≠w→z∩w=∅→∀z∈x∃!vv∈z∩ran⁡f
81 80 imp4b ⊢fFnx∧∀w∈xw≠∅→f⁡w∈w→∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∀z∈x∃!vv∈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→∃!vv∈z∩y↔∃!vv∈z∩ran⁡f
87 86 ralbidv ⊢y=ran⁡f→∀z∈x∃!vv∈z∩y↔∀z∈x∃!vv∈z∩ran⁡f
88 83 87 spcev ⊢∀z∈x∃!vv∈z∩ran⁡f→∃y∀z∈x∃!vv∈z∩y
89 81 88 syl6 ⊢fFnx∧∀w∈xw≠∅→f⁡w∈w→∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y
90 89 exlimiv ⊢∃ffFnx∧∀w∈xw≠∅→f⁡w∈w→∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y
91 90 alimi ⊢∀x∃ffFnx∧∀w∈xw≠∅→f⁡w∈w→∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y
92 1 91 sylbi ⊢CHOICE→∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y
93 eqid ⊢u|u≠∅∧∃t∈hu=t×t=u|u≠∅∧∃t∈hu=t×t
94 eqid ⊢⋃u|u≠∅∧∃t∈hu=t×t∩y=⋃u|u≠∅∧∃t∈hu=t×t∩y
95 biid ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y↔∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y
96 93 94 95 dfac5lem5 ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y→∃f∀w∈hw≠∅→f⁡w∈w
97 96 alrimiv ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y→∀h∃f∀w∈hw≠∅→f⁡w∈w
98 dfac3 ⊢CHOICE↔∀h∃f∀w∈hw≠∅→f⁡w∈w
99 97 98 sylibr ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y→CHOICE
100 92 99 impbii ⊢CHOICE↔∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y