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

Theorem txcls 17628
 Description: Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.)
Assertion
Ref Expression
txcls TopOn TopOn

Proof of Theorem txcls
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 topontop 16983 . . . . . 6 TopOn
21ad2antrr 707 . . . . 5 TopOn TopOn
3 simprl 733 . . . . . 6 TopOn TopOn
4 toponuni 16984 . . . . . . 7 TopOn
54ad2antrr 707 . . . . . 6 TopOn TopOn
63, 5sseqtrd 3376 . . . . 5 TopOn TopOn
7 eqid 2435 . . . . . 6
87clscld 17103 . . . . 5
92, 6, 8syl2anc 643 . . . 4 TopOn TopOn
10 topontop 16983 . . . . . 6 TopOn
1110ad2antlr 708 . . . . 5 TopOn TopOn
12 simprr 734 . . . . . 6 TopOn TopOn
13 toponuni 16984 . . . . . . 7 TopOn
1413ad2antlr 708 . . . . . 6 TopOn TopOn
1512, 14sseqtrd 3376 . . . . 5 TopOn TopOn
16 eqid 2435 . . . . . 6
1716clscld 17103 . . . . 5
1811, 15, 17syl2anc 643 . . . 4 TopOn TopOn
19 txcld 17627 . . . 4
209, 18, 19syl2anc 643 . . 3 TopOn TopOn
217sscls 17112 . . . . 5
222, 6, 21syl2anc 643 . . . 4 TopOn TopOn
2316sscls 17112 . . . . 5
2411, 15, 23syl2anc 643 . . . 4 TopOn TopOn
25 xpss12 4973 . . . 4
2622, 24, 25syl2anc 643 . . 3 TopOn TopOn
27 eqid 2435 . . . 4
2827clsss2 17128 . . 3
2920, 26, 28syl2anc 643 . 2 TopOn TopOn
30 relxp 4975 . . . 4
3130a1i 11 . . 3 TopOn TopOn
32 opelxp 4900 . . . 4
33 eltx 17592 . . . . . . . . 9 TopOn TopOn
3433ad2antrr 707 . . . . . . . 8 TopOn TopOn
35 eleq1 2495 . . . . . . . . . . . . 13
3635anbi1d 686 . . . . . . . . . . . 12
37362rexbidv 2740 . . . . . . . . . . 11
3837rspccva 3043 . . . . . . . . . 10
392ad2antrr 707 . . . . . . . . . . . . . . 15 TopOn TopOn
406ad2antrr 707 . . . . . . . . . . . . . . 15 TopOn TopOn
41 simplrl 737 . . . . . . . . . . . . . . 15 TopOn TopOn
42 simprll 739 . . . . . . . . . . . . . . 15 TopOn TopOn
43 simprrl 741 . . . . . . . . . . . . . . . . 17 TopOn TopOn
44 opelxp 4900 . . . . . . . . . . . . . . . . 17
4543, 44sylib 189 . . . . . . . . . . . . . . . 16 TopOn TopOn
4645simpld 446 . . . . . . . . . . . . . . 15 TopOn TopOn
477clsndisj 17131 . . . . . . . . . . . . . . 15
4839, 40, 41, 42, 46, 47syl32anc 1192 . . . . . . . . . . . . . 14 TopOn TopOn
49 n0 3629 . . . . . . . . . . . . . 14
5048, 49sylib 189 . . . . . . . . . . . . 13 TopOn TopOn
5111ad2antrr 707 . . . . . . . . . . . . . . 15 TopOn TopOn
5215ad2antrr 707 . . . . . . . . . . . . . . 15 TopOn TopOn
53 simplrr 738 . . . . . . . . . . . . . . 15 TopOn TopOn
54 simprlr 740 . . . . . . . . . . . . . . 15 TopOn TopOn
5545simprd 450 . . . . . . . . . . . . . . 15 TopOn TopOn
5616clsndisj 17131 . . . . . . . . . . . . . . 15
5751, 52, 53, 54, 55, 56syl32anc 1192 . . . . . . . . . . . . . 14 TopOn TopOn
58 n0 3629 . . . . . . . . . . . . . 14
5957, 58sylib 189 . . . . . . . . . . . . 13 TopOn TopOn
60 eeanv 1937 . . . . . . . . . . . . . 14
61 inss1 3553 . . . . . . . . . . . . . . . . . . 19
62 opelxpi 4902 . . . . . . . . . . . . . . . . . . . 20
63 inxp 4999 . . . . . . . . . . . . . . . . . . . 20
6462, 63syl6eleqr 2526 . . . . . . . . . . . . . . . . . . 19
6561, 64sseldi 3338 . . . . . . . . . . . . . . . . . 18
66 simprrr 742 . . . . . . . . . . . . . . . . . . 19 TopOn TopOn
6766sselda 3340 . . . . . . . . . . . . . . . . . 18 TopOn TopOn
6865, 67sylan2 461 . . . . . . . . . . . . . . . . 17 TopOn TopOn
69 inss2 3554 . . . . . . . . . . . . . . . . . . 19
7069, 64sseldi 3338 . . . . . . . . . . . . . . . . . 18
7170adantl 453 . . . . . . . . . . . . . . . . 17 TopOn TopOn
72 inelcm 3674 . . . . . . . . . . . . . . . . 17
7368, 71, 72syl2anc 643 . . . . . . . . . . . . . . . 16 TopOn TopOn
7473ex 424 . . . . . . . . . . . . . . 15 TopOn TopOn
7574exlimdvv 1647 . . . . . . . . . . . . . 14 TopOn TopOn
7660, 75syl5bir 210 . . . . . . . . . . . . 13 TopOn TopOn
7750, 59, 76mp2and 661 . . . . . . . . . . . 12 TopOn TopOn
7877expr 599 . . . . . . . . . . 11 TopOn TopOn
7978rexlimdvva 2829 . . . . . . . . . 10 TopOn TopOn
8038, 79syl5 30 . . . . . . . . 9 TopOn TopOn
8180exp3a 426 . . . . . . . 8 TopOn TopOn
8234, 81sylbid 207 . . . . . . 7 TopOn TopOn
8382ralrimiv 2780 . . . . . 6 TopOn TopOn
84 txtopon 17615 . . . . . . . . 9 TopOn TopOn TopOn
8584ad2antrr 707 . . . . . . . 8 TopOn TopOn TopOn
86 topontop 16983 . . . . . . . 8 TopOn
8785, 86syl 16 . . . . . . 7 TopOn TopOn
88 xpss12 4973 . . . . . . . . 9
8988ad2antlr 708 . . . . . . . 8 TopOn TopOn
90 toponuni 16984 . . . . . . . . 9 TopOn
9185, 90syl 16 . . . . . . . 8 TopOn TopOn
9289, 91sseqtrd 3376 . . . . . . 7 TopOn TopOn
937clsss3 17115 . . . . . . . . . . . . 13
942, 6, 93syl2anc 643 . . . . . . . . . . . 12 TopOn TopOn
9594, 5sseqtr4d 3377 . . . . . . . . . . 11 TopOn TopOn
9695sselda 3340 . . . . . . . . . 10 TopOn TopOn
9796adantrr 698 . . . . . . . . 9 TopOn TopOn
9816clsss3 17115 . . . . . . . . . . . . 13
9911, 15, 98syl2anc 643 . . . . . . . . . . . 12 TopOn TopOn
10099, 14sseqtr4d 3377 . . . . . . . . . . 11 TopOn TopOn
101100sselda 3340 . . . . . . . . . 10 TopOn TopOn
102101adantrl 697 . . . . . . . . 9 TopOn TopOn
103 opelxpi 4902 . . . . . . . . 9
10497, 102, 103syl2anc 643 . . . . . . . 8 TopOn TopOn
105104, 91eleqtrd 2511 . . . . . . 7 TopOn TopOn
10627elcls 17129 . . . . . . 7
10787, 92, 105, 106syl3anc 1184 . . . . . 6 TopOn TopOn
10883, 107mpbird 224 . . . . 5 TopOn TopOn
109108ex 424 . . . 4 TopOn TopOn
11032, 109syl5bi 209 . . 3 TopOn TopOn
11131, 110relssdv 4960 . 2 TopOn TopOn
11229, 111eqssd 3357 1 TopOn TopOn
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wex 1550   wceq 1652   wcel 1725   wne 2598  wral 2697  wrex 2698   cin 3311   wss 3312  c0 3620  cop 3809  cuni 4007   cxp 4868   wrel 4875  cfv 5446  (class class class)co 6073  ctop 16950  TopOnctopon 16951  ccld 17072  ccl 17074   ctx 17584 This theorem is referenced by:  clssubg  18130 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-iin 4088  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-topgen 13659  df-top 16955  df-bases 16957  df-topon 16958  df-cld 17075  df-ntr 17076  df-cls 17077  df-tx 17586
 Copyright terms: Public domain W3C validator