Step |
Hyp |
Ref |
Expression |
1 |
|
dfrdg3 |
|
2 |
|
an12 |
|
3 |
|
df-fn |
|
4 |
|
ancom |
|
5 |
|
eqcom |
|
6 |
5
|
anbi1i |
|
7 |
3 4 6
|
3bitri |
|
8 |
7
|
anbi1i |
|
9 |
|
anass |
|
10 |
2 8 9
|
3bitri |
|
11 |
10
|
exbii |
|
12 |
|
vex |
|
13 |
12
|
dmex |
|
14 |
|
eleq1 |
|
15 |
|
raleq |
|
16 |
14 15
|
anbi12d |
|
17 |
16
|
anbi2d |
|
18 |
13 17
|
ceqsexv |
|
19 |
11 18
|
bitri |
|
20 |
|
df-rex |
|
21 |
|
eldif |
|
22 |
|
elin |
|
23 |
12
|
elfuns |
|
24 |
12
|
elima |
|
25 |
|
df-rex |
|
26 |
|
vex |
|
27 |
26 12
|
brcnv |
|
28 |
12 26
|
brdomain |
|
29 |
27 28
|
bitri |
|
30 |
29
|
anbi1ci |
|
31 |
30
|
exbii |
|
32 |
13 14
|
ceqsexv |
|
33 |
31 32
|
bitri |
|
34 |
24 25 33
|
3bitri |
|
35 |
23 34
|
anbi12i |
|
36 |
22 35
|
bitri |
|
37 |
36
|
anbi1i |
|
38 |
|
brdif |
|
39 |
|
vex |
|
40 |
12 39
|
brco |
|
41 |
28
|
anbi1i |
|
42 |
41
|
exbii |
|
43 |
|
breq1 |
|
44 |
13 43
|
ceqsexv |
|
45 |
42 44
|
bitri |
|
46 |
13 39
|
brcnv |
|
47 |
13
|
epeli |
|
48 |
46 47
|
bitri |
|
49 |
40 45 48
|
3bitri |
|
50 |
49
|
anbi1i |
|
51 |
38 50
|
bitri |
|
52 |
|
onelon |
|
53 |
52
|
3adant1 |
|
54 |
|
brun |
|
55 |
|
brxp |
|
56 |
|
opelxp |
|
57 |
12 56
|
mpbiran |
|
58 |
|
velsn |
|
59 |
57 58
|
bitri |
|
60 |
|
velsn |
|
61 |
59 60
|
anbi12i |
|
62 |
55 61
|
bitri |
|
63 |
|
brun |
|
64 |
26
|
brresi |
|
65 |
|
opelxp |
|
66 |
12 65
|
mpbiran |
|
67 |
39
|
ellimits |
|
68 |
66 67
|
bitri |
|
69 |
|
opex |
|
70 |
69 26
|
brco |
|
71 |
|
vex |
|
72 |
12 39 71
|
brimg |
|
73 |
26
|
brbigcup |
|
74 |
72 73
|
anbi12i |
|
75 |
74
|
exbii |
|
76 |
12
|
imaex |
|
77 |
|
unieq |
|
78 |
77
|
eqeq1d |
|
79 |
76 78
|
ceqsexv |
|
80 |
|
eqcom |
|
81 |
79 80
|
bitri |
|
82 |
70 75 81
|
3bitri |
|
83 |
68 82
|
anbi12i |
|
84 |
64 83
|
bitri |
|
85 |
26
|
brresi |
|
86 |
|
opelxp |
|
87 |
12 86
|
mpbiran |
|
88 |
39
|
elrn |
|
89 |
71 39
|
brsuccf |
|
90 |
89
|
exbii |
|
91 |
87 88 90
|
3bitri |
|
92 |
69 26
|
brco |
|
93 |
|
vex |
|
94 |
69 93
|
brco |
|
95 |
12 39 71
|
brpprod3a |
|
96 |
|
3anrot |
|
97 |
93
|
ideq |
|
98 |
|
equcom |
|
99 |
97 98
|
bitri |
|
100 |
|
vex |
|
101 |
100
|
brbigcup |
|
102 |
|
eqcom |
|
103 |
101 102
|
bitri |
|
104 |
|
biid |
|
105 |
99 103 104
|
3anbi123i |
|
106 |
96 105
|
bitri |
|
107 |
106
|
2exbii |
|
108 |
|
vuniex |
|
109 |
|
opeq1 |
|
110 |
109
|
eqeq2d |
|
111 |
|
opeq2 |
|
112 |
111
|
eqeq2d |
|
113 |
12 108 110 112
|
ceqsex2v |
|
114 |
95 107 113
|
3bitri |
|
115 |
114
|
anbi1i |
|
116 |
115
|
exbii |
|
117 |
|
opex |
|
118 |
|
breq1 |
|
119 |
117 118
|
ceqsexv |
|
120 |
12 108 93
|
brapply |
|
121 |
119 120
|
bitri |
|
122 |
94 116 121
|
3bitri |
|
123 |
93 26
|
brfullfun |
|
124 |
122 123
|
anbi12i |
|
125 |
124
|
exbii |
|
126 |
|
fvex |
|
127 |
|
fveq2 |
|
128 |
127
|
eqeq2d |
|
129 |
126 128
|
ceqsexv |
|
130 |
92 125 129
|
3bitri |
|
131 |
91 130
|
anbi12i |
|
132 |
85 131
|
bitri |
|
133 |
84 132
|
orbi12i |
|
134 |
63 133
|
bitri |
|
135 |
62 134
|
orbi12i |
|
136 |
54 135
|
bitri |
|
137 |
|
onzsl |
|
138 |
|
nlim0 |
|
139 |
|
limeq |
|
140 |
138 139
|
mtbiri |
|
141 |
140
|
intnanrd |
|
142 |
|
nsuceq0 |
|
143 |
|
neeq2 |
|
144 |
142 143
|
mpbiri |
|
145 |
144
|
necomd |
|
146 |
145
|
neneqd |
|
147 |
146
|
nexdv |
|
148 |
147
|
intnanrd |
|
149 |
|
ioran |
|
150 |
141 148 149
|
sylanbrc |
|
151 |
|
orel2 |
|
152 |
150 151
|
syl |
|
153 |
|
iftrue |
|
154 |
|
unisnif |
|
155 |
153 154
|
eqtr4di |
|
156 |
155
|
eqeq2d |
|
157 |
156
|
biimprd |
|
158 |
157
|
adantld |
|
159 |
152 158
|
syld |
|
160 |
156
|
biimpd |
|
161 |
160
|
anc2li |
|
162 |
|
orc |
|
163 |
161 162
|
syl6 |
|
164 |
159 163
|
impbid |
|
165 |
|
neeq1 |
|
166 |
142 165
|
mpbiri |
|
167 |
166
|
neneqd |
|
168 |
167
|
intnanrd |
|
169 |
168
|
rexlimivw |
|
170 |
|
orel1 |
|
171 |
169 170
|
syl |
|
172 |
|
nlimsucg |
|
173 |
172
|
elv |
|
174 |
|
limeq |
|
175 |
173 174
|
mtbiri |
|
176 |
175
|
rexlimivw |
|
177 |
176
|
intnanrd |
|
178 |
|
orel1 |
|
179 |
177 178
|
syl |
|
180 |
142
|
neii |
|
181 |
180
|
iffalsei |
|
182 |
|
iffalse |
|
183 |
71 172 182
|
mp2b |
|
184 |
181 183
|
eqtri |
|
185 |
|
eqeq1 |
|
186 |
|
unieq |
|
187 |
186
|
fveq2d |
|
188 |
187
|
fveq2d |
|
189 |
174 188
|
ifbieq2d |
|
190 |
185 189
|
ifbieq2d |
|
191 |
184 190 188
|
3eqtr4a |
|
192 |
191
|
rexlimivw |
|
193 |
192
|
eqeq2d |
|
194 |
193
|
biimprd |
|
195 |
194
|
adantld |
|
196 |
171 179 195
|
3syld |
|
197 |
|
rexex |
|
198 |
193
|
biimpd |
|
199 |
|
olc |
|
200 |
199
|
olcd |
|
201 |
197 198 200
|
syl6an |
|
202 |
196 201
|
impbid |
|
203 |
140
|
con2i |
|
204 |
203
|
intnanrd |
|
205 |
204 170
|
syl |
|
206 |
175
|
exlimiv |
|
207 |
206
|
con2i |
|
208 |
207
|
intnanrd |
|
209 |
|
orel2 |
|
210 |
208 209
|
syl |
|
211 |
203
|
iffalsed |
|
212 |
|
iftrue |
|
213 |
211 212
|
eqtrd |
|
214 |
213
|
eqeq2d |
|
215 |
214
|
biimprd |
|
216 |
215
|
adantld |
|
217 |
205 210 216
|
3syld |
|
218 |
217
|
adantl |
|
219 |
214
|
biimpd |
|
220 |
219
|
anc2li |
|
221 |
|
orc |
|
222 |
221
|
olcd |
|
223 |
220 222
|
syl6 |
|
224 |
223
|
adantl |
|
225 |
218 224
|
impbid |
|
226 |
164 202 225
|
3jaoi |
|
227 |
137 226
|
sylbi |
|
228 |
136 227
|
syl5bb |
|
229 |
53 228
|
syl |
|
230 |
26 69
|
brcnv |
|
231 |
12 39 26
|
brapply |
|
232 |
230 231
|
bitri |
|
233 |
232
|
a1i |
|
234 |
229 233
|
anbi12d |
|
235 |
234
|
biancomd |
|
236 |
235
|
exbidv |
|
237 |
|
df-br |
|
238 |
69
|
elfix |
|
239 |
69 69
|
brco |
|
240 |
237 238 239
|
3bitri |
|
241 |
|
fvex |
|
242 |
241
|
eqvinc |
|
243 |
236 240 242
|
3bitr4g |
|
244 |
243
|
notbid |
|
245 |
244
|
3expia |
|
246 |
245
|
pm5.32d |
|
247 |
|
annim |
|
248 |
246 247
|
bitrdi |
|
249 |
51 248
|
syl5bb |
|
250 |
249
|
exbidv |
|
251 |
|
exnal |
|
252 |
250 251
|
bitr2di |
|
253 |
12
|
eldm |
|
254 |
252 253
|
bitr4di |
|
255 |
254
|
con1bid |
|
256 |
|
df-ral |
|
257 |
255 256
|
bitr4di |
|
258 |
257
|
pm5.32i |
|
259 |
|
anass |
|
260 |
258 259
|
bitri |
|
261 |
21 37 260
|
3bitri |
|
262 |
19 20 261
|
3bitr4ri |
|
263 |
262
|
abbi2i |
|
264 |
263
|
unieqi |
|
265 |
1 264
|
eqtr4i |
|