Metamath Proof Explorer


Theorem dfac14

Description: Theorem ptcls is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion dfac14 CHOICEff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfksk

Proof

Step Hyp Ref Expression
1 fveq2 k=xfk=fx
2 1 unieqd k=xfk=fx
3 2 pweqd k=x𝒫fk=𝒫fx
4 3 cbvixpv kdomf𝒫fk=xdomf𝒫fx
5 4 eleq2i skdomf𝒫fksxdomf𝒫fx
6 simplr CHOICEf:domfTopsxdomf𝒫fxf:domfTop
7 6 feqmptd CHOICEf:domfTopsxdomf𝒫fxf=kdomffk
8 7 fveq2d CHOICEf:domfTopsxdomf𝒫fx𝑡f=𝑡kdomffk
9 8 fveq2d CHOICEf:domfTopsxdomf𝒫fxcls𝑡f=cls𝑡kdomffk
10 9 fveq1d CHOICEf:domfTopsxdomf𝒫fxcls𝑡fkdomfsk=cls𝑡kdomffkkdomfsk
11 eqid 𝑡kdomffk=𝑡kdomffk
12 vex fV
13 12 dmex domfV
14 13 a1i CHOICEf:domfTopsxdomf𝒫fxdomfV
15 6 ffvelrnda CHOICEf:domfTopsxdomf𝒫fxkdomffkTop
16 toptopon2 fkTopfkTopOnfk
17 15 16 sylib CHOICEf:domfTopsxdomf𝒫fxkdomffkTopOnfk
18 simpr CHOICEf:domfTopsxdomf𝒫fxsxdomf𝒫fx
19 18 5 sylibr CHOICEf:domfTopsxdomf𝒫fxskdomf𝒫fk
20 vex sV
21 20 elixp skdomf𝒫fksFndomfkdomfsk𝒫fk
22 21 simprbi skdomf𝒫fkkdomfsk𝒫fk
23 19 22 syl CHOICEf:domfTopsxdomf𝒫fxkdomfsk𝒫fk
24 23 r19.21bi CHOICEf:domfTopsxdomf𝒫fxkdomfsk𝒫fk
25 24 elpwid CHOICEf:domfTopsxdomf𝒫fxkdomfskfk
26 fvex skV
27 13 26 iunex kdomfskV
28 simpll CHOICEf:domfTopsxdomf𝒫fxCHOICE
29 acacni CHOICEdomfVAC_domf=V
30 28 13 29 sylancl CHOICEf:domfTopsxdomf𝒫fxAC_domf=V
31 27 30 eleqtrrid CHOICEf:domfTopsxdomf𝒫fxkdomfskAC_domf
32 11 14 17 25 31 ptclsg CHOICEf:domfTopsxdomf𝒫fxcls𝑡kdomffkkdomfsk=kdomfclsfksk
33 10 32 eqtrd CHOICEf:domfTopsxdomf𝒫fxcls𝑡fkdomfsk=kdomfclsfksk
34 5 33 sylan2b CHOICEf:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfksk
35 34 ralrimiva CHOICEf:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfksk
36 35 ex CHOICEf:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfksk
37 36 alrimiv CHOICEff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfksk
38 vex gV
39 38 dmex domgV
40 39 a1i ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangdomgV
41 fvex gxV
42 41 a1i ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomggxV
43 simplrr ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomgrang
44 df-nel rang¬rang
45 43 44 sylib ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomg¬rang
46 funforn Fungg:domgontorang
47 fof g:domgontorangg:domgrang
48 46 47 sylbi Fungg:domgrang
49 48 ad2antrl ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangg:domgrang
50 49 ffvelrnda ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomggxrang
51 eleq1 gx=gxrangrang
52 50 51 syl5ibcom ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomggx=rang
53 52 necon3bd ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomg¬ranggx
54 45 53 mpd ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomggx
55 eqid 𝒫gx=𝒫gx
56 eqid y𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx=y𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx
57 eqid 𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx=𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx
58 fveq1 s=gsk=gk
59 58 ixpeq2dv s=gkdomgsk=kdomggk
60 fveq2 k=xgk=gx
61 60 cbvixpv kdomggk=xdomggx
62 59 61 eqtrdi s=gkdomgsk=xdomggx
63 62 fveq2d s=gcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgsk=cls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxxdomggx
64 58 fveq2d s=gclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk=clsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gkgk
65 64 ixpeq2dv s=gkdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gkgk
66 60 unieqd k=xgk=gx
67 66 pweqd k=x𝒫gk=𝒫gx
68 67 sneqd k=x𝒫gk=𝒫gx
69 60 68 uneq12d k=xgk𝒫gk=gx𝒫gx
70 69 pweqd k=x𝒫gk𝒫gk=𝒫gx𝒫gx
71 67 eleq1d k=x𝒫gky𝒫gxy
72 69 eqeq2d k=xy=gk𝒫gky=gx𝒫gx
73 71 72 imbi12d k=x𝒫gkyy=gk𝒫gk𝒫gxyy=gx𝒫gx
74 70 73 rabeqbidv k=xy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gk=y𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx
75 74 fveq2d k=xclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gk=clsy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx
76 75 60 fveq12d k=xclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gkgk=clsy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxgx
77 76 cbvixpv kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gkgk=xdomgclsy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxgx
78 65 77 eqtrdi s=gkdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk=xdomgclsy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxgx
79 63 78 eqeq12d s=gcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgsk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gkskcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxxdomggx=xdomgclsy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxgx
80 simpl ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfksk
81 snex 𝒫gxV
82 41 81 unex gx𝒫gxV
83 ssun2 𝒫gxgx𝒫gx
84 41 uniex gxV
85 84 pwex 𝒫gxV
86 85 snid 𝒫gx𝒫gx
87 83 86 sselii 𝒫gxgx𝒫gx
88 epttop gx𝒫gxV𝒫gxgx𝒫gxy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxTopOngx𝒫gx
89 82 87 88 mp2an y𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxTopOngx𝒫gx
90 89 topontopi y𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxTop
91 90 a1i ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxTop
92 91 fmpttd ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx:domgTop
93 39 mptex xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxV
94 id f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxf=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx
95 dmeq f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxdomf=domxdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx
96 82 pwex 𝒫gx𝒫gxV
97 96 rabex y𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxV
98 eqid xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx
99 97 98 dmmpti domxdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx=domg
100 95 99 eqtrdi f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxdomf=domg
101 94 100 feq12d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxf:domfTopxdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx:domgTop
102 100 ixpeq1d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomf𝒫fk=kdomg𝒫fk
103 fveq1 f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxfk=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxk
104 fveq2 x=kgx=gk
105 104 unieqd x=kgx=gk
106 105 pweqd x=k𝒫gx=𝒫gk
107 106 sneqd x=k𝒫gx=𝒫gk
108 104 107 uneq12d x=kgx𝒫gx=gk𝒫gk
109 108 pweqd x=k𝒫gx𝒫gx=𝒫gk𝒫gk
110 106 eleq1d x=k𝒫gxy𝒫gky
111 108 eqeq2d x=ky=gx𝒫gxy=gk𝒫gk
112 110 111 imbi12d x=k𝒫gxyy=gx𝒫gx𝒫gkyy=gk𝒫gk
113 109 112 rabeqbidv x=ky𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx=y𝒫gk𝒫gk|𝒫gkyy=gk𝒫gk
114 fvex gkV
115 snex 𝒫gkV
116 114 115 unex gk𝒫gkV
117 116 pwex 𝒫gk𝒫gkV
118 117 rabex y𝒫gk𝒫gk|𝒫gkyy=gk𝒫gkV
119 113 98 118 fvmpt kdomgxdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxk=y𝒫gk𝒫gk|𝒫gkyy=gk𝒫gk
120 103 119 sylan9eq f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgfk=y𝒫gk𝒫gk|𝒫gkyy=gk𝒫gk
121 120 unieqd f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgfk=y𝒫gk𝒫gk|𝒫gkyy=gk𝒫gk
122 ssun2 𝒫gkgk𝒫gk
123 114 uniex gkV
124 123 pwex 𝒫gkV
125 124 snid 𝒫gk𝒫gk
126 122 125 sselii 𝒫gkgk𝒫gk
127 epttop gk𝒫gkV𝒫gkgk𝒫gky𝒫gk𝒫gk|𝒫gkyy=gk𝒫gkTopOngk𝒫gk
128 116 126 127 mp2an y𝒫gk𝒫gk|𝒫gkyy=gk𝒫gkTopOngk𝒫gk
129 128 toponunii gk𝒫gk=y𝒫gk𝒫gk|𝒫gkyy=gk𝒫gk
130 121 129 eqtr4di f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgfk=gk𝒫gk
131 130 pweqd f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomg𝒫fk=𝒫gk𝒫gk
132 131 ixpeq2dva f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomg𝒫fk=kdomg𝒫gk𝒫gk
133 102 132 eqtrd f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomf𝒫fk=kdomg𝒫gk𝒫gk
134 2fveq3 f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxcls𝑡f=cls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx
135 100 ixpeq1d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomfsk=kdomgsk
136 134 135 fveq12d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxcls𝑡fkdomfsk=cls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgsk
137 100 ixpeq1d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomfclsfksk=kdomgclsfksk
138 120 fveq2d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgclsfk=clsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gk
139 138 fveq1d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgclsfksk=clsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk
140 139 ixpeq2dva f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgclsfksk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk
141 137 140 eqtrd f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomfclsfksk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk
142 136 141 eqeq12d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxcls𝑡fkdomfsk=kdomfclsfkskcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgsk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk
143 133 142 raleqbidv f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskskdomg𝒫gk𝒫gkcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgsk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk
144 101 143 imbi12d f=xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxf:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskxdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx:domgTopskdomg𝒫gk𝒫gkcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgsk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk
145 93 144 spcv ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskxdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gx:domgTopskdomg𝒫gk𝒫gkcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgsk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk
146 80 92 145 sylc ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangskdomg𝒫gk𝒫gkcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxkdomgsk=kdomgclsy𝒫gk𝒫gk|𝒫gkyy=gk𝒫gksk
147 simprl ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangFung
148 147 funfnd ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungranggFndomg
149 ssun1 gkgk𝒫gk
150 114 elpw gk𝒫gk𝒫gkgkgk𝒫gk
151 149 150 mpbir gk𝒫gk𝒫gk
152 151 rgenw kdomggk𝒫gk𝒫gk
153 38 elixp gkdomg𝒫gk𝒫gkgFndomgkdomggk𝒫gk𝒫gk
154 148 152 153 sylanblrc ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungranggkdomg𝒫gk𝒫gk
155 79 146 154 rspcdva ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangcls𝑡xdomgy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxxdomggx=xdomgclsy𝒫gx𝒫gx|𝒫gxyy=gx𝒫gxgx
156 40 42 54 55 56 57 155 dfac14lem ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomggx
157 156 ex ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskFungrangxdomggx
158 157 alrimiv ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskgFungrangxdomggx
159 dfac9 CHOICEgFungrangxdomggx
160 158 159 sylibr ff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfkskCHOICE
161 37 160 impbii CHOICEff:domfTopskdomf𝒫fkcls𝑡fkdomfsk=kdomfclsfksk