Metamath Proof Explorer


Theorem dfac2b

Description: Axiom of Choice (first form) of Enderton p. 49 implies our Axiom of Choice (in the form of ac3 ). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq and preleq that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a .) (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 16-Jun-2022)

Ref Expression
Assertion dfac2b CHOICE x y z x z ∃! w z v y z v w v

Proof

Step Hyp Ref Expression
1 dfac3 CHOICE x f z x z f z z
2 nfra1 z z x z f z z
3 rsp z x z f z z z x z f z z
4 equid z = z
5 neeq1 u = z u z
6 eqeq1 u = z u = z z = z
7 5 6 anbi12d u = z u u = z z z = z
8 7 rspcev z x z z = z u x u u = z
9 4 8 mpanr2 z x z u x u u = z
10 fveq2 u = z f u = f z
11 10 preq1d u = z f u u = f z u
12 preq2 u = z f z u = f z z
13 11 12 eqtr2d u = z f z z = f u u
14 13 anim2i u u = z u f z z = f u u
15 14 reximi u x u u = z u x u f z z = f u u
16 9 15 syl z x z u x u f z z = f u u
17 prex f z z V
18 eqeq1 g = f z z g = f u u f z z = f u u
19 18 anbi2d g = f z z u g = f u u u f z z = f u u
20 19 rexbidv g = f z z u x u g = f u u u x u f z z = f u u
21 17 20 elab f z z g | u x u g = f u u u x u f z z = f u u
22 16 21 sylibr z x z f z z g | u x u g = f u u
23 vex z V
24 23 prid2 z f z z
25 fvex f z V
26 25 prid1 f z f z z
27 24 26 pm3.2i z f z z f z f z z
28 eleq2 v = f z z z v z f z z
29 eleq2 v = f z z f z v f z f z z
30 28 29 anbi12d v = f z z z v f z v z f z z f z f z z
31 30 rspcev f z z g | u x u g = f u u z f z z f z f z z v g | u x u g = f u u z v f z v
32 22 27 31 sylancl z x z v g | u x u g = f u u z v f z v
33 eleq1 w = f z w z f z z
34 eleq1 w = f z w v f z v
35 34 anbi2d w = f z z v w v z v f z v
36 35 rexbidv w = f z v g | u x u g = f u u z v w v v g | u x u g = f u u z v f z v
37 33 36 anbi12d w = f z w z v g | u x u g = f u u z v w v f z z v g | u x u g = f u u z v f z v
38 25 37 spcev f z z v g | u x u g = f u u z v f z v w w z v g | u x u g = f u u z v w v
39 32 38 sylan2 f z z z x z w w z v g | u x u g = f u u z v w v
40 39 ex f z z z x z w w z v g | u x u g = f u u z v w v
41 3 40 syl8 z x z f z z z x z z x z w w z v g | u x u g = f u u z v w v
42 41 impd z x z f z z z x z z x z w w z v g | u x u g = f u u z v w v
43 42 pm2.43d z x z f z z z x z w w z v g | u x u g = f u u z v w v
44 df-rex v g | u x u g = f u u z v w v v v g | u x u g = f u u z v w v
45 vex v V
46 eqeq1 g = v g = f u u v = f u u
47 46 anbi2d g = v u g = f u u u v = f u u
48 47 rexbidv g = v u x u g = f u u u x u v = f u u
49 45 48 elab v g | u x u g = f u u u x u v = f u u
50 neeq1 z = u z u
51 fveq2 z = u f z = f u
52 51 eleq1d z = u f z z f u z
53 eleq2 z = u f u z f u u
54 52 53 bitrd z = u f z z f u u
55 50 54 imbi12d z = u z f z z u f u u
56 55 rspccv z x z f z z u x u f u u
57 elneq w z w z
58 57 neneqd w z ¬ w = z
59 vex w V
60 neqne ¬ w = z w z
61 prel12g w V z V w z w z = f u u w f u u z f u u
62 59 23 60 61 mp3an12i ¬ w = z w z = f u u w f u u z f u u
63 eleq2 v = f u u w v w f u u
64 eleq2 v = f u u z v z f u u
65 63 64 anbi12d v = f u u w v z v w f u u z f u u
66 ancom w v z v z v w v
67 65 66 bitr3di v = f u u w f u u z f u u z v w v
68 62 67 sylan9bbr v = f u u ¬ w = z w z = f u u z v w v
69 58 68 sylan2 v = f u u w z w z = f u u z v w v
70 69 adantrr v = f u u w z f u u w z = f u u z v w v
71 70 pm5.32da v = f u u w z f u u w z = f u u w z f u u z v w v
72 23 preleq w z f u u w z = f u u w = f u z = u
73 71 72 syl6bir v = f u u w z f u u z v w v w = f u z = u
74 51 eqeq2d z = u w = f z w = f u
75 74 biimparc w = f u z = u w = f z
76 73 75 syl6 v = f u u w z f u u z v w v w = f z
77 76 exp4c v = f u u w z f u u z v w v w = f z
78 77 com13 f u u w z v = f u u z v w v w = f z
79 56 78 syl8 z x z f z z u x u w z v = f u u z v w v w = f z
80 79 com4r w z z x z f z z u x u v = f u u z v w v w = f z
81 80 imp w z z x z f z z u x u v = f u u z v w v w = f z
82 81 imp4a w z z x z f z z u x u v = f u u z v w v w = f z
83 82 com3l u x u v = f u u w z z x z f z z z v w v w = f z
84 83 rexlimiv u x u v = f u u w z z x z f z z z v w v w = f z
85 49 84 sylbi v g | u x u g = f u u w z z x z f z z z v w v w = f z
86 85 expd v g | u x u g = f u u w z z x z f z z z v w v w = f z
87 86 com13 z x z f z z w z v g | u x u g = f u u z v w v w = f z
88 87 imp4b z x z f z z w z v g | u x u g = f u u z v w v w = f z
89 88 exlimdv z x z f z z w z v v g | u x u g = f u u z v w v w = f z
90 44 89 syl5bi z x z f z z w z v g | u x u g = f u u z v w v w = f z
91 90 expimpd z x z f z z w z v g | u x u g = f u u z v w v w = f z
92 91 alrimiv z x z f z z w w z v g | u x u g = f u u z v w v w = f z
93 mo2icl w w z v g | u x u g = f u u z v w v w = f z * w w z v g | u x u g = f u u z v w v
94 92 93 syl z x z f z z * w w z v g | u x u g = f u u z v w v
95 43 94 jctird z x z f z z z x z w w z v g | u x u g = f u u z v w v * w w z v g | u x u g = f u u z v w v
96 df-reu ∃! w z v g | u x u g = f u u z v w v ∃! w w z v g | u x u g = f u u z v w v
97 df-eu ∃! w w z v g | u x u g = f u u z v w v w w z v g | u x u g = f u u z v w v * w w z v g | u x u g = f u u z v w v
98 96 97 bitri ∃! w z v g | u x u g = f u u z v w v w w z v g | u x u g = f u u z v w v * w w z v g | u x u g = f u u z v w v
99 95 98 syl6ibr z x z f z z z x z ∃! w z v g | u x u g = f u u z v w v
100 99 expd z x z f z z z x z ∃! w z v g | u x u g = f u u z v w v
101 2 100 ralrimi z x z f z z z x z ∃! w z v g | u x u g = f u u z v w v
102 vex f V
103 102 rnex ran f V
104 p0ex V
105 103 104 unex ran f V
106 vex x V
107 105 106 unex ran f x V
108 107 pwex 𝒫 ran f x V
109 ssun1 ran f ran f x
110 fvrn0 f u ran f
111 109 110 sselii f u ran f x
112 elun2 u x u ran f x
113 prssi f u ran f x u ran f x f u u ran f x
114 111 112 113 sylancr u x f u u ran f x
115 prex f u u V
116 115 elpw f u u 𝒫 ran f x f u u ran f x
117 114 116 sylibr u x f u u 𝒫 ran f x
118 eleq1 g = f u u g 𝒫 ran f x f u u 𝒫 ran f x
119 117 118 syl5ibrcom u x g = f u u g 𝒫 ran f x
120 119 adantld u x u g = f u u g 𝒫 ran f x
121 120 rexlimiv u x u g = f u u g 𝒫 ran f x
122 121 abssi g | u x u g = f u u 𝒫 ran f x
123 108 122 ssexi g | u x u g = f u u V
124 rexeq y = g | u x u g = f u u v y z v w v v g | u x u g = f u u z v w v
125 124 reubidv y = g | u x u g = f u u ∃! w z v y z v w v ∃! w z v g | u x u g = f u u z v w v
126 125 imbi2d y = g | u x u g = f u u z ∃! w z v y z v w v z ∃! w z v g | u x u g = f u u z v w v
127 126 ralbidv y = g | u x u g = f u u z x z ∃! w z v y z v w v z x z ∃! w z v g | u x u g = f u u z v w v
128 123 127 spcev z x z ∃! w z v g | u x u g = f u u z v w v y z x z ∃! w z v y z v w v
129 101 128 syl z x z f z z y z x z ∃! w z v y z v w v
130 129 exlimiv f z x z f z z y z x z ∃! w z v y z v w v
131 130 alimi x f z x z f z z x y z x z ∃! w z v y z v w v
132 1 131 sylbi CHOICE x y z x z ∃! w z v y z v w v