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

Theorem ptbasfi 17615
 Description: The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add itself to the list because if is empty we get while .) (Contributed by Mario Carneiro, 3-Feb-2015.)
Hypotheses
Ref Expression
ptbas.1
ptbasfi.2
Assertion
Ref Expression
ptbasfi
Distinct variable groups:   ,,,   ,,,,,,,,   ,,,,,,,,   ,,,,,,   ,,,,,,,,
Allowed substitution hints:   (,,,,)   (,)

Proof of Theorem ptbasfi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptbas.1 . . . . 5
21elpt 17606 . . . 4
3 df-3an 939 . . . . . . . 8
4 simprr 735 . . . . . . . . . . . . . 14
5 difeq2 3461 . . . . . . . . . . . . . . . . . . 19
6 difin 3580 . . . . . . . . . . . . . . . . . . 19
7 dif0 3700 . . . . . . . . . . . . . . . . . . 19
85, 6, 73eqtr3g 2493 . . . . . . . . . . . . . . . . . 18
98raleqdv 2912 . . . . . . . . . . . . . . . . 17
109biimpac 474 . . . . . . . . . . . . . . . 16
11 ixpeq2 7078 . . . . . . . . . . . . . . . 16
1210, 11syl 16 . . . . . . . . . . . . . . 15
13 ptbasfi.2 . . . . . . . . . . . . . . . 16
14 fveq2 5730 . . . . . . . . . . . . . . . . . 18
1514unieqd 4028 . . . . . . . . . . . . . . . . 17
1615cbvixpv 7082 . . . . . . . . . . . . . . . 16
1713, 16eqtri 2458 . . . . . . . . . . . . . . 15
1812, 17syl6eqr 2488 . . . . . . . . . . . . . 14
194, 18sylan 459 . . . . . . . . . . . . 13
20 ssv 3370 . . . . . . . . . . . . . . . 16
21 iineq1 4109 . . . . . . . . . . . . . . . . 17
22 0iin 4151 . . . . . . . . . . . . . . . . 17
2321, 22syl6eq 2486 . . . . . . . . . . . . . . . 16
2420, 23syl5sseqr 3399 . . . . . . . . . . . . . . 15
2524adantl 454 . . . . . . . . . . . . . 14
26 df-ss 3336 . . . . . . . . . . . . . 14
2725, 26sylib 190 . . . . . . . . . . . . 13
2819, 27eqtr4d 2473 . . . . . . . . . . . 12
29 simplll 736 . . . . . . . . . . . . . . . 16
30 inss1 3563 . . . . . . . . . . . . . . . . 17
31 simpr 449 . . . . . . . . . . . . . . . . 17
3230, 31sseldi 3348 . . . . . . . . . . . . . . . 16
33 simprr 735 . . . . . . . . . . . . . . . . . 18
3433ad2antrr 708 . . . . . . . . . . . . . . . . 17
35 fveq2 5730 . . . . . . . . . . . . . . . . . . 19
36 fveq2 5730 . . . . . . . . . . . . . . . . . . 19
3735, 36eleq12d 2506 . . . . . . . . . . . . . . . . . 18
3837rspcv 3050 . . . . . . . . . . . . . . . . 17
3932, 34, 38sylc 59 . . . . . . . . . . . . . . . 16
4017ptpjpre1 17605 . . . . . . . . . . . . . . . 16
4129, 32, 39, 40syl12anc 1183 . . . . . . . . . . . . . . 15
4241adantlr 697 . . . . . . . . . . . . . 14
4342iineq2dv 4117 . . . . . . . . . . . . 13
44 simpr 449 . . . . . . . . . . . . . . . . 17
45 cnvimass 5226 . . . . . . . . . . . . . . . . . . . 20
46 eqid 2438 . . . . . . . . . . . . . . . . . . . . 21
4746dmmptss 5368 . . . . . . . . . . . . . . . . . . . 20
4845, 47sstri 3359 . . . . . . . . . . . . . . . . . . 19
4948, 17sseqtri 3382 . . . . . . . . . . . . . . . . . 18
5049rgenw 2775 . . . . . . . . . . . . . . . . 17
51 r19.2z 3719 . . . . . . . . . . . . . . . . 17
5244, 50, 51sylancl 645 . . . . . . . . . . . . . . . 16
53 iinss 4144 . . . . . . . . . . . . . . . 16
5452, 53syl 16 . . . . . . . . . . . . . . 15
5554, 17syl6sseqr 3397 . . . . . . . . . . . . . 14
56 dfss1 3547 . . . . . . . . . . . . . 14
5755, 56sylib 190 . . . . . . . . . . . . 13
5833ad2antrr 708 . . . . . . . . . . . . . . . . 17
59 ssralv 3409 . . . . . . . . . . . . . . . . . 18
6030, 59ax-mp 8 . . . . . . . . . . . . . . . . 17
61 elssuni 4045 . . . . . . . . . . . . . . . . . . . . . . . 24
62 iffalse 3748 . . . . . . . . . . . . . . . . . . . . . . . . 25
6362sseq2d 3378 . . . . . . . . . . . . . . . . . . . . . . . 24
6461, 63syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . . . 23
65 ssid 3369 . . . . . . . . . . . . . . . . . . . . . . . 24
66 iftrue 3747 . . . . . . . . . . . . . . . . . . . . . . . . 25
6766, 35eqtr4d 2473 . . . . . . . . . . . . . . . . . . . . . . . 24
6865, 67syl5sseqr 3399 . . . . . . . . . . . . . . . . . . . . . . 23
6964, 68pm2.61d2 155 . . . . . . . . . . . . . . . . . . . . . 22
7069ralrimivw 2792 . . . . . . . . . . . . . . . . . . . . 21
71 ssiin 4143 . . . . . . . . . . . . . . . . . . . . 21
7270, 71sylibr 205 . . . . . . . . . . . . . . . . . . . 20
7372adantl 454 . . . . . . . . . . . . . . . . . . 19
7466equcoms 1694 . . . . . . . . . . . . . . . . . . . . . . . . 25
75 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . 25
7674, 75eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . 24
7776sseq1d 3377 . . . . . . . . . . . . . . . . . . . . . . 23
7877rspcev 3054 . . . . . . . . . . . . . . . . . . . . . 22
7965, 78mpan2 654 . . . . . . . . . . . . . . . . . . . . 21
80 iinss 4144 . . . . . . . . . . . . . . . . . . . . 21
8179, 80syl 16 . . . . . . . . . . . . . . . . . . . 20
8281adantr 453 . . . . . . . . . . . . . . . . . . 19
8373, 82eqssd 3367 . . . . . . . . . . . . . . . . . 18
8483ralimiaa 2782 . . . . . . . . . . . . . . . . 17
8558, 60, 843syl 19 . . . . . . . . . . . . . . . 16
86 eldifn 3472 . . . . . . . . . . . . . . . . . . . . . . . 24
8786ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23
88 inss2 3564 . . . . . . . . . . . . . . . . . . . . . . . . 25
89 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . 25
9088, 89sseldi 3348 . . . . . . . . . . . . . . . . . . . . . . . 24
91 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . 24
9290, 91syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . . . 23
9387, 92mtod 171 . . . . . . . . . . . . . . . . . . . . . 22
9493, 62syl 16 . . . . . . . . . . . . . . . . . . . . 21
9594iineq2dv 4117 . . . . . . . . . . . . . . . . . . . 20
96 iinconst 4104 . . . . . . . . . . . . . . . . . . . . 21
9796adantr 453 . . . . . . . . . . . . . . . . . . . 20
9895, 97eqtr2d 2471 . . . . . . . . . . . . . . . . . . 19
99 eqeq1 2444 . . . . . . . . . . . . . . . . . . 19
10098, 99syl5ibrcom 215 . . . . . . . . . . . . . . . . . 18
101100ralimdva 2786 . . . . . . . . . . . . . . . . 17
1024, 101mpan9 457 . . . . . . . . . . . . . . . 16
103 inundif 3708 . . . . . . . . . . . . . . . . . 18
104103raleqi 2910 . . . . . . . . . . . . . . . . 17
105 ralunb 3530 . . . . . . . . . . . . . . . . 17
106104, 105bitr3i 244 . . . . . . . . . . . . . . . 16
10785, 102, 106sylanbrc 647 . . . . . . . . . . . . . . 15
108 ixpeq2 7078 . . . . . . . . . . . . . . 15
109107, 108syl 16 . . . . . . . . . . . . . 14
110 ixpiin 7090 . . . . . . . . . . . . . . 15
111110adantl 454 . . . . . . . . . . . . . 14
112109, 111eqtrd 2470 . . . . . . . . . . . . 13
11343, 57, 1123eqtr4rd 2481 . . . . . . . . . . . 12
11428, 113pm2.61dane 2684 . . . . . . . . . . 11
115 ixpexg 7088 . . . . . . . . . . . . . . . . . . . . . . . 24
116 fvex 5744 . . . . . . . . . . . . . . . . . . . . . . . . . 26
117116uniex 4707 . . . . . . . . . . . . . . . . . . . . . . . . 25
118117a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
119115, 118mprg 2777 . . . . . . . . . . . . . . . . . . . . . . 23
12013, 119eqeltri 2508 . . . . . . . . . . . . . . . . . . . . . 22
121120mptex 5968 . . . . . . . . . . . . . . . . . . . . 21
122121cnvex 5408 . . . . . . . . . . . . . . . . . . . 20
123 imaexg 5219 . . . . . . . . . . . . . . . . . . . 20
124122, 123ax-mp 8 . . . . . . . . . . . . . . . . . . 19
125124dfiin2 4128 . . . . . . . . . . . . . . . . . 18
126 inteq 4055 . . . . . . . . . . . . . . . . . 18
127125, 126syl5eq 2482 . . . . . . . . . . . . . . . . 17
128 int0 4066 . . . . . . . . . . . . . . . . 17
129127, 128syl6eq 2486 . . . . . . . . . . . . . . . 16
130129ineq2d 3544 . . . . . . . . . . . . . . 15
131 inv1 3656 . . . . . . . . . . . . . . 15
132130, 131syl6eq 2486 . . . . . . . . . . . . . 14
133132adantl 454 . . . . . . . . . . . . 13
134 snex 4407 . . . . . . . . . . . . . . . . . 18
1351ptbas 17613 . . . . . . . . . . . . . . . . . . 19
1361, 13ptpjpre2 17614 . . . . . . . . . . . . . . . . . . . . . 22
137136ralrimivva 2800 . . . . . . . . . . . . . . . . . . . . 21
138 eqid 2438 . . . . . . . . . . . . . . . . . . . . . 22
139138fmpt2x 6419 . . . . . . . . . . . . . . . . . . . . 21
140137, 139sylib 190 . . . . . . . . . . . . . . . . . . . 20
141 frn 5599 . . . . . . . . . . . . . . . . . . . 20
142140, 141syl 16 . . . . . . . . . . . . . . . . . . 19
143135, 142ssexd 4352 . . . . . . . . . . . . . . . . . 18
144 unexg 4712 . . . . . . . . . . . . . . . . . 18
145134, 143, 144sylancr 646 . . . . . . . . . . . . . . . . 17
146 ssfii 7426 . . . . . . . . . . . . . . . . 17
147145, 146syl 16 . . . . . . . . . . . . . . . 16
148147ad2antrr 708 . . . . . . . . . . . . . . 15
149 ssun1 3512 . . . . . . . . . . . . . . . . 17
150120snss 3928 . . . . . . . . . . . . . . . . 17
151149, 150mpbir 202 . . . . . . . . . . . . . . . 16
152151a1i 11 . . . . . . . . . . . . . . 15
153148, 152sseldd 3351 . . . . . . . . . . . . . 14
154153adantr 453 . . . . . . . . . . . . 13
155133, 154eqeltrd 2512 . . . . . . . . . . . 12
156145ad3antrrr 712 . . . . . . . . . . . . . . . . . 18
157 nfv 1630 . . . . . . . . . . . . . . . . . . . . . 22
158 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . 25
159 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . 25
160 nfixp1 7084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
16113, 160nfcxfr 2571 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
162 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
163161, 162nfmpt 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
164163nfcnv 5053 . . . . . . . . . . . . . . . . . . . . . . . . . 26
165 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . . 26
166164, 165nfima 5213 . . . . . . . . . . . . . . . . . . . . . . . . 25
167158, 159, 166nfmpt2 6144 . . . . . . . . . . . . . . . . . . . . . . . 24
168167nfrn 5114 . . . . . . . . . . . . . . . . . . . . . . 23
169168nfcri 2568 . . . . . . . . . . . . . . . . . . . . . 22
170 df-ov 6086 . . . . . . . . . . . . . . . . . . . . . . . . . 26
171124a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
172 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
173172mpteq2dv 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
174173cnveqd 5050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
175174imaeq1d 5204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
176 imaeq2 5201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
177175, 176sylan9eq 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
178 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179177, 178, 138ovmpt2x 6204 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
18032, 39, 171, 179syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . 26
181170, 180syl5eqr 2484 . . . . . . . . . . . . . . . . . . . . . . . . 25
182140ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
183 ffn 5593 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
184182, 183syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
185 opeliunxp 4931 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
18632, 39, 185sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
187 sneq 3827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
188 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
189187, 188xpeq12d 4905 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
190189cbviunv 4132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
191186, 190syl6eleq 2528 . . . . . . . . . . . . . . . . . . . . . . . . . 26
192 fnfvelrn 5869 . . . . . . . . . . . . . . . . . . . . . . . . . 26
193184, 191, 192syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 25
194181, 193eqeltrrd 2513 . . . . . . . . . . . . . . . . . . . . . . . 24
195 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . 24
196194, 195syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . . . 23
197196ex 425 . . . . . . . . . . . . . . . . . . . . . 22
198157, 169, 197rexlimd 2829 . . . . . . . . . . . . . . . . . . . . 21
199198abssdv 3419 . . . . . . . . . . . . . . . . . . . 20
200 ssun2 3513 . . . . . . . . . . . . . . . . . . . 20
201199, 200syl6ss 3362 . . . . . . . . . . . . . . . . . . 19
202201adantr 453 . . . . . . . . . . . . . . . . . 18
203 simpr 449 . . . . . . . . . . . . . . . . . 18
204 simplrl 738 . . . . . . . . . . . . . . . . . . . 20
205 ssfi 7331 . . . . . . . . . . . . . . . . . . . 20
206204, 88, 205sylancl 645 . . . . . . . . . . . . . . . . . . 19
207 abrexfi 7409 . . . . . . . . . . . . . . . . . . 19
208206, 207syl 16 . . . . . . . . . . . . . . . . . 18
209 elfir 7422 . . . . . . . . . . . . . . . . . 18
210156, 202, 203, 208, 209syl13anc 1187 . . . . . . . . . . . . . . . . 17
211125, 210syl5eqel 2522 . . . . . . . . . . . . . . . 16
212 elssuni 4045 . . . . . . . . . . . . . . . 16
213211, 212syl 16 . . . . . . . . . . . . . . 15
214 fiuni 7435 . . . . . . . . . . . . . . . . . 18
215145, 214syl 16 . . . . . . . . . . . . . . . . 17
216120pwid 3814 . . . . . . . . . . . . . . . . . . . . . 22
217216a1i 11 . . . . . . . . . . . . . . . . . . . . 21
218217snssd 3945 . . . . . . . . . . . . . . . . . . . 20
2191ptuni2 17610 . . . . . . . . . . . . . . . . . . . . . . . 24
22013, 219syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . 23
221 eqimss2 3403 . . . . . . . . . . . . . . . . . . . . . . 23
222220, 221syl 16 . . . . . . . . . . . . . . . . . . . . . 22
223 sspwuni 4178 . . . . . . . . . . . . . . . . . . . . . 22
224222, 223sylibr 205 . . . . . . . . . . . . . . . . . . . . 21
225142, 224sstrd 3360 . . . . . . . . . . . . . . . . . . . 20
226218, 225unssd 3525 . . . . . . . . . . . . . . . . . . 19
227 sspwuni 4178 . . . . . . . . . . . . . . . . . . 19
228226, 227sylib 190 . . . . . . . . . . . . . . . . . 18
229 elssuni 4045 . . . . . . . . . . . . . . . . . . . 20
230151, 229ax-mp 8 . . . . . . . . . . . . . . . . . . 19
231230a1i 11 . . . . . . . . . . . . . . . . . 18
232228, 231eqssd 3367 . . . . . . . . . . . . . . . . 17
233215, 232eqtr3d 2472 . . . . . . . . . . . . . . . 16
234233ad3antrrr 712 . . . . . . . . . . . . . . 15
235213, 234sseqtrd 3386 . . . . . . . . . . . . . 14
236235, 56sylib 190 . . . . . . . . . . . . 13
237236, 211eqeltrd 2512 . . . . . . . . . . . 12
238155, 237pm2.61dane 2684 . . . . . . . . . . 11
239114, 238eqeltrd 2512 . . . . . . . . . 10
240239rexlimdvaa 2833 . . . . . . . . 9
241240impr 604 . . . . . . . 8
2423, 241sylan2b 463 . . . . . . 7