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 bitrdi 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