Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  alexsubALTlem3 Unicode version

Theorem alexsubALTlem3 18033
 Description: Lemma for alexsubALT 18035. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)
Hypothesis
Ref Expression
alexsubALT.1
Assertion
Ref Expression
alexsubALTlem3
Distinct variable groups:   ,,,,,,,,,,,   ,,,,,,,,,,,

Proof of Theorem alexsubALTlem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfrex2 2679 . . . . . . . . . . 11
21ralbii 2690 . . . . . . . . . 10
3 ralnex 2676 . . . . . . . . . 10
42, 3bitr2i 242 . . . . . . . . 9
5 elin 3490 . . . . . . . . . . . . . . . . . . 19
6 elpwi 3767 . . . . . . . . . . . . . . . . . . . . . . 23
76adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
8 uncom 3451 . . . . . . . . . . . . . . . . . . . . . 22
97, 8syl6sseq 3354 . . . . . . . . . . . . . . . . . . . . 21
10 ssundif 3671 . . . . . . . . . . . . . . . . . . . . 21
119, 10sylib 189 . . . . . . . . . . . . . . . . . . . 20
12 diffi 7298 . . . . . . . . . . . . . . . . . . . . 21
1312adantl 453 . . . . . . . . . . . . . . . . . . . 20
1411, 13jca 519 . . . . . . . . . . . . . . . . . . 19
155, 14sylbi 188 . . . . . . . . . . . . . . . . . 18
1615adantr 452 . . . . . . . . . . . . . . . . 17
1716ad2antll 710 . . . . . . . . . . . . . . . 16
18 elin 3490 . . . . . . . . . . . . . . . . 17
19 vex 2919 . . . . . . . . . . . . . . . . . . 19
2019elpw2 4324 . . . . . . . . . . . . . . . . . 18
2120anbi1i 677 . . . . . . . . . . . . . . . . 17
2218, 21bitr2i 242 . . . . . . . . . . . . . . . 16
2317, 22sylib 189 . . . . . . . . . . . . . . 15
24 simprrr 742 . . . . . . . . . . . . . . . . 17
25 eldif 3290 . . . . . . . . . . . . . . . . . . . . . 22
2625simplbi2 609 . . . . . . . . . . . . . . . . . . . . 21
27 elun 3448 . . . . . . . . . . . . . . . . . . . . . . 23
28 orcom 377 . . . . . . . . . . . . . . . . . . . . . . 23
2927, 28bitr4i 244 . . . . . . . . . . . . . . . . . . . . . 22
30 df-or 360 . . . . . . . . . . . . . . . . . . . . . 22
3129, 30bitr2i 242 . . . . . . . . . . . . . . . . . . . . 21
3226, 31sylib 189 . . . . . . . . . . . . . . . . . . . 20
3332ssriv 3312 . . . . . . . . . . . . . . . . . . 19
34 uniss 3996 . . . . . . . . . . . . . . . . . . 19
3533, 34mp1i 12 . . . . . . . . . . . . . . . . . 18
36 uniun 3994 . . . . . . . . . . . . . . . . . . 19
37 vex 2919 . . . . . . . . . . . . . . . . . . . . 21
3837unisn 3991 . . . . . . . . . . . . . . . . . . . 20
3938uneq2i 3458 . . . . . . . . . . . . . . . . . . 19
4036, 39eqtri 2424 . . . . . . . . . . . . . . . . . 18
4135, 40syl6sseq 3354 . . . . . . . . . . . . . . . . 17
4224, 41eqsstrd 3342 . . . . . . . . . . . . . . . 16
43 difss 3434 . . . . . . . . . . . . . . . . . . . . 21
4443unissi 3998 . . . . . . . . . . . . . . . . . . . 20
45 sseq2 3330 . . . . . . . . . . . . . . . . . . . 20
4644, 45mpbiri 225 . . . . . . . . . . . . . . . . . . 19
4746adantl 453 . . . . . . . . . . . . . . . . . 18
4847ad2antll 710 . . . . . . . . . . . . . . . . 17
49 inss1 3521 . . . . . . . . . . . . . . . . . . . . . . . 24
5049sseli 3304 . . . . . . . . . . . . . . . . . . . . . . 23
5150elpwid 3768 . . . . . . . . . . . . . . . . . . . . . 22
5251ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . 21
5352ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20
54 simprl 733 . . . . . . . . . . . . . . . . . . . 20
5553, 54sseldd 3309 . . . . . . . . . . . . . . . . . . 19
56 elssuni 4003 . . . . . . . . . . . . . . . . . . 19
5755, 56syl 16 . . . . . . . . . . . . . . . . . 18
58 fibas 16997 . . . . . . . . . . . . . . . . . . . . 21
59 unitg 16987 . . . . . . . . . . . . . . . . . . . . 21
6058, 59mp1i 12 . . . . . . . . . . . . . . . . . . . 20
61 unieq 3984 . . . . . . . . . . . . . . . . . . . . . 22
62613ad2ant1 978 . . . . . . . . . . . . . . . . . . . . 21
6362ad3antrrr 711 . . . . . . . . . . . . . . . . . . . 20
64 vex 2919 . . . . . . . . . . . . . . . . . . . . 21
65 fiuni 7391 . . . . . . . . . . . . . . . . . . . . 21
6664, 65mp1i 12 . . . . . . . . . . . . . . . . . . . 20
6760, 63, 663eqtr4rd 2447 . . . . . . . . . . . . . . . . . . 19
68 alexsubALT.1 . . . . . . . . . . . . . . . . . . 19
6967, 68syl6eqr 2454 . . . . . . . . . . . . . . . . . 18
7057, 69sseqtrd 3344 . . . . . . . . . . . . . . . . 17
7148, 70unssd 3483 . . . . . . . . . . . . . . . 16
7242, 71eqssd 3325 . . . . . . . . . . . . . . 15
73 unieq 3984 . . . . . . . . . . . . . . . . . 18
7473uneq1d 3460 . . . . . . . . . . . . . . . . 17
7574eqeq2d 2415 . . . . . . . . . . . . . . . 16
7675rspcev 3012 . . . . . . . . . . . . . . 15
7723, 72, 76syl2anc 643 . . . . . . . . . . . . . 14
7877expr 599 . . . . . . . . . . . . 13
7978exp3a 426 . . . . . . . . . . . 12
8079rexlimdv 2789 . . . . . . . . . . 11
8180ralimdva 2744 . . . . . . . . . 10
82 inss2 3522 . . . . . . . . . . . . . . 15
8382sseli 3304 . . . . . . . . . . . . . 14
8483adantr 452 . . . . . . . . . . . . 13
85 unieq 3984 . . . . . . . . . . . . . . . . 17
8685uneq1d 3460 . . . . . . . . . . . . . . . 16
8786eqeq2d 2415 . . . . . . . . . . . . . . 15
8887ac6sfi 7310 . . . . . . . . . . . . . 14
8988ex 424 . . . . . . . . . . . . 13
9084, 89syl 16 . . . . . . . . . . . 12
9190adantr 452 . . . . . . . . . . 11
9291ad2antrl 709 . . . . . . . . . 10
93 ffvelrn 5827 . . . . . . . . . . . . . . . . . . . 20
94 elin 3490 . . . . . . . . . . . . . . . . . . . . 21
95 elpwi 3767 . . . . . . . . . . . . . . . . . . . . . 22
9695adantr 452 . . . . . . . . . . . . . . . . . . . . 21
9794, 96sylbi 188 . . . . . . . . . . . . . . . . . . . 20
9893, 97syl 16 . . . . . . . . . . . . . . . . . . 19
9998ralrimiva 2749 . . . . . . . . . . . . . . . . . 18
100 iunss 4092 . . . . . . . . . . . . . . . . . 18
10199, 100sylibr 204 . . . . . . . . . . . . . . . . 17
102101ad2antrl 709 . . . . . . . . . . . . . . . 16
103 simplrr 738 . . . . . . . . . . . . . . . . 17
104103snssd 3903 . . . . . . . . . . . . . . . 16
105102, 104unssd 3483 . . . . . . . . . . . . . . 15
106 inss2 3522 . . . . . . . . . . . . . . . . . . . . . 22
107106, 93sseldi 3306 . . . . . . . . . . . . . . . . . . . . 21
108107ralrimiva 2749 . . . . . . . . . . . . . . . . . . . 20
109 iunfi 7353 . . . . . . . . . . . . . . . . . . . 20
11084, 108, 109syl2an 464 . . . . . . . . . . . . . . . . . . 19
111110adantlr 696 . . . . . . . . . . . . . . . . . 18
112111adantlr 696 . . . . . . . . . . . . . . . . 17
113112ad2ant2lr 729 . . . . . . . . . . . . . . . 16
114 snfi 7146 . . . . . . . . . . . . . . . 16
115 unfi 7333 . . . . . . . . . . . . . . . 16
116113, 114, 115sylancl 644 . . . . . . . . . . . . . . 15
117105, 116jca 519 . . . . . . . . . . . . . 14
118 elin 3490 . . . . . . . . . . . . . . 15
11919elpw2 4324 . . . . . . . . . . . . . . . 16
120119anbi1i 677 . . . . . . . . . . . . . . 15
121118, 120bitr2i 242 . . . . . . . . . . . . . 14
122117, 121sylib 189 . . . . . . . . . . . . 13
123 ralnex 2676 . . . . . . . . . . . . . . . . . . . . . . . . . 26
124123imbi2i 304 . . . . . . . . . . . . . . . . . . . . . . . . 25
125124albii 1572 . . . . . . . . . . . . . . . . . . . . . . . 24
126 alinexa 1585 . . . . . . . . . . . . . . . . . . . . . . . 24
127125, 126bitr2i 242 . . . . . . . . . . . . . . . . . . . . . . 23
128 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
129128unieqd 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
130 id 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
131129, 130uneq12d 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
132131eqeq2d 2415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
133132rspcv 3008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134 eleq2 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
135134biimpd 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
136 elun 3448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
137 eluni 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
138137orbi1i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
139 df-or 360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
140 alinexa 1585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
141140imbi1i 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
142139, 141bitr4i 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
143136, 138, 1423bitri 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
144 eleq2 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
145 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
146145notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
147146ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
148144, 147imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
149148spv 1963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
150128eleq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
151150notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
152151rspcv 3008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
153149, 152syl9r 69 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
154153alrimdv 1640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
155154imim1d 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
156143, 155syl5bi 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
157156a1dd 44 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
158135, 157syl9r 69 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
159133, 158syld 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
160159com14 84 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
161160imp31 422 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
162161com23 74 . . . . . . . . . . . . . . . . . . . . . . . . . 26
163162ralrimdv 2755 . . . . . . . . . . . . . . . . . . . . . . . . 25
164 vex 2919 . . . . . . . . . . . . . . . . . . . . . . . . . 26
165164elint2 4017 . . . . . . . . . . . . . . . . . . . . . . . . 25
166163, 165syl6ibr 219 . . . . . . . . . . . . . . . . . . . . . . . 24
167 eleq2 2465 . . . . . . . . . . . . . . . . . . . . . . . . 25
168167ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24
169166, 168sylibrd 226 . . . . . . . . . . . . . . . . . . . . . . 23
170127, 169syl5bi 209 . . . . . . . . . . . . . . . . . . . . . 22
171170orrd 368 . . . . . . . . . . . . . . . . . . . . 21
172171ex 424 . . . . . . . . . . . . . . . . . . . 20
173 orc 375 . . . . . . . . . . . . . . . . . . . . . . . 24
174173anim2i 553 . . . . . . . . . . . . . . . . . . . . . . 23
175174eximi 1582 . . . . . . . . . . . . . . . . . . . . . 22
176 equid 1684 . . . . . . . . . . . . . . . . . . . . . . . 24
177 vex 2919 . . . . . . . . . . . . . . . . . . . . . . . . 25
178 equequ1 1692 . . . . . . . . . . . . . . . . . . . . . . . . . 26
179144, 178anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . 25
180177, 179spcev 3003 . . . . . . . . . . . . . . . . . . . . . . . 24
181176, 180mpan2 653 . . . . . . . . . . . . . . . . . . . . . . 23
182 olc 374 . . . . . . . . . . . . . . . . . . . . . . . . 25
183182anim2i 553 . . . . . . . . . . . . . . . . . . . . . . . 24
184183eximi 1582 . . . . . . . . . . . . . . . . . . . . . . 23
185181, 184syl 16 . . . . . . . . . . . . . . . . . . . . . 22
186175, 185jaoi 369 . . . . . . . . . . . . . . . . . . . . 21
187 eluni 3978 . . . . . . . . . . . . . . . . . . . . . 22
188 elun 3448 . . . . . . . . . . . . . . . . . . . . . . . . 25
189 eliun 4057 . . . . . . . . . . . . . . . . . . . . . . . . . 26
190 elsn 3789 . . . . . . . . . . . . . . . . . . . . . . . . . 26
191189, 190orbi12i 508 . . . . . . . . . . . . . . . . . . . . . . . . 25
192188, 191bitri 241 . . . . . . . . . . . . . . . . . . . . . . . 24
193192anbi2i 676 . . . . . . . . . . . . . . . . . . . . . . 23
194193exbii 1589 . . . . . . . . . . . . . . . . . . . . . 22
195187, 194bitr2i 242 . . . . . . . . . . . . . . . . . . . . 21
196186, 195sylib 189 . . . . . . . . . . . . . . . . . . . 20
197172, 196syl6 31 . . . . . . . . . . . . . . . . . . 19
198197adantll 695 . . . . . . . . . . . . . . . . . 18
199198adantlr 696 . . . . . . . . . . . . . . . . 17
200199adantlr 696 . . . . . . . . . . . . . . . 16
201200ad2ant2l 727 . . . . . . . . . . . . . . 15
202201ssrdv 3314 . . . . . . . . . . . . . 14
203 elun 3448 . . . . . . . . . . . . . . . . . 18
204 eliun 4057 . . . . . . . . . . . . . . . . . . 19
205 elsn 3789 . . . . . . . . . . . . . . . . . . 19
206204, 205orbi12i 508 . . . . . . . . . . . . . . . . . 18
207203, 206bitri 241 . . . . . . . . . . . . . . . . 17
208 nfra1 2716 . . . . . . . . . . . . . . . . . . . 20
209 nfv 1626 . . . . . . . . . . . . . . . . . . . 20
210 rsp 2726 . . . . . . . . . . . . . . . . . . . . 21
211 eqimss2 3361 . . . . . . . . . . . . . . . . . . . . . 22
212 elssuni 4003 . . . . . . . . . . . . . . . . . . . . . . 23
213 ssun3 3472 . . . . . . . . . . . . . . . . . . . . . . 23
214212, 213syl 16 . . . . . . . . . . . . . . . . . . . . . 22
215 sstr 3316 . . . . . . . . . . . . . . . . . . . . . . 23
216215expcom 425 . . . . . . . . . . . . . . . . . . . . . 22
217211, 214, 216syl2im 36 . . . . . . . . . . . . . . . . . . . . 21
218210, 217syl6 31 . . . . . . . . . . . . . . . . . . . 20
219208, 209, 218rexlimd 2787 . . . . . . . . . . . . . . . . . . 19
220219ad2antll 710 . . . . . . . . . . . . . . . . . 18
221 elpwi 3767 . . . . . . . . . . . . . . . . . . . . . . . 24
222221ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . 23
223222ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
224223, 103sseldd 3309 . . . . . . . . . . . . . . . . . . . . 21
225 elssuni 4003 . . . . . . . . . . . . . . . . . . . . 21
226224, 225syl 16 . . . . . . . . . . . . . . . . . . . 20
22758, 59ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24
22861, 227syl6req 2453 . . . . . . . . . . . . . . . . . . . . . . 23
229228, 68syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . . 22
2302293ad2ant1 978 . . . . . . . . . . . . . . . . . . . . 21
231230ad3antrrr 711 . . . . . . . . . . . . . . . . . . . 20
232226, 231sseqtrd 3344 . . . . . . . . . . . . . . . . . . 19
233 sseq1 3329 . . . . . . . . . . . . . . . . . . 19
234232, 233syl5ibrcom 214 . . . . . . . . . . . . . . . . . 18
235220, 234jaod 370 . . . . . . . . . . . . . . . . 17
236207, 235syl5bi 209 . . . . . . . . . . . . . . . 16
237236ralrimiv 2748 . . . . . . . . . . . . . . 15
238 unissb 4005 . . . . . . . . . . . . . . 15
239237, 238sylibr 204 . . . . . . . . . . . . . 14
240202, 239eqssd 3325 . . . . . . . . . . . . 13
241 unieq 3984 . . . . . . . . . . . . . . 15
242241eqeq2d 2415 . . . . . . . . . . . . . 14
243242rspcev 3012 . . . . . . . . . . . . 13
244122, 240, 243syl2anc 643 . . . . . . . . . . . 12
245244ex 424 . . . . . . . . . . 11
246245exlimdv 1643 . . . . . . . . . 10
24781, 92, 2463syld 53 . . . . . . . . 9
2484, 247syl5bi 209 . . . . . . . 8
249 dfrex2 2679 . . . . . . . 8
250248, 249syl6ib 218 . . . . . . 7
251250con4d 99 . . . . . 6
252251exp32 589 . . . . 5
253252com24 83 . . . 4
254253exp32 589 . . 3
255254imp45 581 . 2
256255imp31 422 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   w3a 936  wal 1546  wex 1547   wceq 1649   wcel 1721  wral 2666  wrex 2667  cvv 2916   cdif 3277   cun 3278   cin 3279   wss 3280  cpw 3759  csn 3774  cuni 3975  cint 4010  ciun 4053  wf 5409  cfv 5413  cfn 7068  cfi 7373  ctg 13620  ctb 16917 This theorem is referenced by:  alexsubALTlem4  18034 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-fin 7072  df-fi 7374  df-topgen 13622  df-bases 16920
 Copyright terms: Public domain W3C validator