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

Theorem ptclsg 17409
 Description: The closure of a box in the product topology is the box formed from the closures of the factors. The proof uses the axiom of choice; the last hypothesis is the choice assumption. (Contributed by Mario Carneiro, 3-Sep-2015.)
Hypotheses
Ref Expression
ptcls.2
ptcls.a
ptcls.j TopOn
ptcls.c
ptclsg.1 AC
Assertion
Ref Expression
ptclsg
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()

Proof of Theorem ptclsg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcls.a . . . . 5
2 ptcls.j . . . . . 6 TopOn
3 topontop 16764 . . . . . 6 TopOn
42, 3syl 15 . . . . 5
5 ptcls.c . . . . . . 7
6 toponuni 16765 . . . . . . . 8 TopOn
72, 6syl 15 . . . . . . 7
85, 7sseqtrd 3290 . . . . . 6
9 eqid 2358 . . . . . . 7
109clscld 16884 . . . . . 6
114, 8, 10syl2anc 642 . . . . 5
121, 4, 11ptcldmpt 17408 . . . 4
13 ptcls.2 . . . . 5
1413fveq2i 5608 . . . 4
1512, 14syl6eleqr 2449 . . 3
169sscls 16893 . . . . . 6
174, 8, 16syl2anc 642 . . . . 5
1817ralrimiva 2702 . . . 4
19 ss2ixp 6914 . . . 4
2018, 19syl 15 . . 3
21 eqid 2358 . . . 4
2221clsss2 16909 . . 3
2315, 20, 22syl2anc 642 . 2
24 vex 2867 . . . . . . . 8
25 eqeq1 2364 . . . . . . . . . 10
2625anbi2d 684 . . . . . . . . 9
2726exbidv 1626 . . . . . . . 8
2824, 27elab 2990 . . . . . . 7
29 nfmpt1 4188 . . . . . . . . . . . . . . . . . . 19
30 nfcv 2494 . . . . . . . . . . . . . . . . . . 19
3129, 30nffv 5612 . . . . . . . . . . . . . . . . . 18
3231nfel2 2506 . . . . . . . . . . . . . . . . 17
33 nfv 1619 . . . . . . . . . . . . . . . . 17
34 fveq2 5605 . . . . . . . . . . . . . . . . . 18
35 fveq2 5605 . . . . . . . . . . . . . . . . . 18
3634, 35eleq12d 2426 . . . . . . . . . . . . . . . . 17
3732, 33, 36cbvral 2836 . . . . . . . . . . . . . . . 16
38 simpr 447 . . . . . . . . . . . . . . . . . . 19
39 eqid 2358 . . . . . . . . . . . . . . . . . . . 20
4039fvmpt2 5688 . . . . . . . . . . . . . . . . . . 19 TopOn
4138, 2, 40syl2anc 642 . . . . . . . . . . . . . . . . . 18
4241eleq2d 2425 . . . . . . . . . . . . . . . . 17
4342ralbidva 2635 . . . . . . . . . . . . . . . 16
4437, 43syl5bb 248 . . . . . . . . . . . . . . 15
4544anbi2d 684 . . . . . . . . . . . . . 14
4645adantr 451 . . . . . . . . . . . . 13
4746biimpa 470 . . . . . . . . . . . 12
48 ptclsg.1 . . . . . . . . . . . . . . . 16 AC
4948ad2antrr 706 . . . . . . . . . . . . . . 15 AC
50 simpll 730 . . . . . . . . . . . . . . . . . . 19
51 vex 2867 . . . . . . . . . . . . . . . . . . . . . 22
5251elixp 6908 . . . . . . . . . . . . . . . . . . . . 21
5352simprbi 450 . . . . . . . . . . . . . . . . . . . 20
5453ad2antlr 707 . . . . . . . . . . . . . . . . . . 19
559clsndisj 16912 . . . . . . . . . . . . . . . . . . . . . . 23
5655ex 423 . . . . . . . . . . . . . . . . . . . . . 22
57563expia 1153 . . . . . . . . . . . . . . . . . . . . 21
584, 8, 57syl2anc 642 . . . . . . . . . . . . . . . . . . . 20
5958ralimdva 2697 . . . . . . . . . . . . . . . . . . 19
6050, 54, 59sylc 56 . . . . . . . . . . . . . . . . . 18
61 simprlr 739 . . . . . . . . . . . . . . . . . . 19
62 simprr 733 . . . . . . . . . . . . . . . . . . . . 21
6334cbvixpv 6919 . . . . . . . . . . . . . . . . . . . . 21
6462, 63syl6eleq 2448 . . . . . . . . . . . . . . . . . . . 20
6551elixp 6908 . . . . . . . . . . . . . . . . . . . . 21
6665simprbi 450 . . . . . . . . . . . . . . . . . . . 20
6764, 66syl 15 . . . . . . . . . . . . . . . . . . 19
68 r19.26 2751 . . . . . . . . . . . . . . . . . . 19
6961, 67, 68sylanbrc 645 . . . . . . . . . . . . . . . . . 18
70 ralim 2690 . . . . . . . . . . . . . . . . . 18
7160, 69, 70sylc 56 . . . . . . . . . . . . . . . . 17
72 rabn0 3550 . . . . . . . . . . . . . . . . . . 19
73 dfin5 3236 . . . . . . . . . . . . . . . . . . . . 21
74 inss2 3466 . . . . . . . . . . . . . . . . . . . . . . 23
75 ssiun2 4024 . . . . . . . . . . . . . . . . . . . . . . 23
7674, 75syl5ss 3266 . . . . . . . . . . . . . . . . . . . . . 22
77 dfss1 3449 . . . . . . . . . . . . . . . . . . . . . 22
7876, 77sylib 188 . . . . . . . . . . . . . . . . . . . . 21
7973, 78syl5eqr 2404 . . . . . . . . . . . . . . . . . . . 20
8079neeq1d 2534 . . . . . . . . . . . . . . . . . . 19
8172, 80syl5bbr 250 . . . . . . . . . . . . . . . . . 18
8281ralbiia 2651 . . . . . . . . . . . . . . . . 17
8371, 82sylibr 203 . . . . . . . . . . . . . . . 16
84 nfv 1619 . . . . . . . . . . . . . . . . 17
85 nfiu1 4012 . . . . . . . . . . . . . . . . . 18
86 nfcv 2494 . . . . . . . . . . . . . . . . . . . 20
87 nfcsb1v 3189 . . . . . . . . . . . . . . . . . . . 20
8886, 87nfin 3451 . . . . . . . . . . . . . . . . . . 19
8988nfel2 2506 . . . . . . . . . . . . . . . . . 18
9085, 89nfrex 2674 . . . . . . . . . . . . . . . . 17
91 fveq2 5605 . . . . . . . . . . . . . . . . . . . 20
92 csbeq1a 3165 . . . . . . . . . . . . . . . . . . . 20
9391, 92ineq12d 3447 . . . . . . . . . . . . . . . . . . 19
9493eleq2d 2425 . . . . . . . . . . . . . . . . . 18
9594rexbidv 2640 . . . . . . . . . . . . . . . . 17
9684, 90, 95cbvral 2836 . . . . . . . . . . . . . . . 16
9783, 96sylib 188 . . . . . . . . . . . . . . 15
98 eleq1 2418 . . . . . . . . . . . . . . . 16
9998acni3 7761 . . . . . . . . . . . . . . 15 AC
10049, 97, 99syl2anc 642 . . . . . . . . . . . . . 14
101 ffn 5469 . . . . . . . . . . . . . . . 16
102 nfv 1619 . . . . . . . . . . . . . . . . . 18
10388nfel2 2506 . . . . . . . . . . . . . . . . . 18
104 fveq2 5605 . . . . . . . . . . . . . . . . . . 19
105104, 93eleq12d 2426 . . . . . . . . . . . . . . . . . 18
106102, 103, 105cbvral 2836 . . . . . . . . . . . . . . . . 17
107 ne0i 3537 . . . . . . . . . . . . . . . . . 18
108 vex 2867 . . . . . . . . . . . . . . . . . . 19
109108elixp 6908 . . . . . . . . . . . . . . . . . 18
110 ixpin 6926 . . . . . . . . . . . . . . . . . . . 20
11163ineq1i 3442 . . . . . . . . . . . . . . . . . . . 20
112110, 111eqtr4i 2381 . . . . . . . . . . . . . . . . . . 19
113112neeq1i 2531 . . . . . . . . . . . . . . . . . 18
114107, 109, 1133imtr3i 256 . . . . . . . . . . . . . . . . 17
115106, 114sylan2br 462 . . . . . . . . . . . . . . . 16
116101, 115sylan 457 . . . . . . . . . . . . . . 15
117116exlimiv 1634 . . . . . . . . . . . . . 14
118100, 117syl 15 . . . . . . . . . . . . 13
119118expr 598 . . . . . . . . . . . 12
12047, 119syldan 456 . . . . . . . . . . 11
1211203adantr3 1116 . . . . . . . . . 10
122 eleq2 2419 . . . . . . . . . . 11
123 ineq1 3439 . . . . . . . . . . . 12
124123neeq1d 2534 . . . . . . . . . . 11
125122, 124imbi12d 311 . . . . . . . . . 10
126121, 125syl5ibrcom 213 . . . . . . . . 9
127126expimpd 586 . . . . . . . 8
128127exlimdv 1636 . . . . . . 7
12928, 128syl5bi 208 . . . . . 6
130129ralrimiv 2701 . . . . 5
1314, 39fmptd 5764 . . . . . . . . . 10
132 ffn 5469 . . . . . . . . . 10
133131, 132syl 15 . . . . . . . . 9
134 eqid 2358 . . . . . . . . . 10
135134ptval 17365 . . . . . . . . 9
1361, 133, 135syl2anc 642 . . . . . . . 8
13713, 136syl5eq 2402 . . . . . . 7
138137adantr 451 . . . . . 6
1392ralrimiva 2702 . . . . . . . . 9 TopOn
14013pttopon 17391 . . . . . . . . 9 TopOn TopOn
1411, 139, 140syl2anc 642 . . . . . . . 8 TopOn
142 toponuni 16765 . . . . . . . 8 TopOn
143141, 142syl 15 . . . . . . 7
144143adantr 451 . . . . . 6
145134ptbas 17374 . . . . . . . 8
1461, 131, 145syl2anc 642 . . . . . . 7
147146adantr 451 . . . . . 6
1485ralrimiva 2702 . . . . . . . 8
149 ss2ixp 6914 . . . . . . . 8
150148, 149syl 15 . . . . . . 7
151150adantr 451 . . . . . 6
1529clsss3 16896 . . . . . . . . . . 11
1534, 8, 152syl2anc 642 . . . . . . . . . 10
154153, 7sseqtr4d 3291 . . . . . . . . 9
155154ralrimiva 2702 . . . . . . . 8
156 ss2ixp 6914 . . . . . . . 8
157155, 156syl 15 . . . . . . 7
158157sselda 3256 . . . . . 6
159138, 144, 147, 151, 158elcls3 16920 . . . . 5
160130, 159mpbird 223 . . . 4
161160ex 423 . . 3
162161ssrdv 3261 . 2
16323, 162eqssd 3272 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wex 1541   wceq 1642   wcel 1710  cab 2344   wne 2521  wral 2619  wrex 2620  crab 2623  csb 3157   cdif 3225   cin 3227   wss 3228  c0 3531  cuni 3906  ciun 3984   cmpt 4156   wfn 5329  wf 5330  cfv 5334  cixp 6902  cfn 6948  AC wacn 7658  ctg 13435  cpt 13436  ctop 16731  TopOnctopon 16732  ctb 16735  ccld 16853  ccl 16855 This theorem is referenced by:  ptcls  17410  dfac14  17412 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4210  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-iin 3987  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-recs 6472  df-rdg 6507  df-1o 6563  df-oadd 6567  df-er 6744  df-map 6859  df-ixp 6903  df-en 6949  df-fin 6952  df-fi 7252  df-acn 7662  df-topgen 13437  df-pt 13438  df-top 16736  df-bases 16738  df-topon 16739  df-cld 16856  df-ntr 16857  df-cls 16858
 Copyright terms: Public domain W3C validator