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

Theorem txcls 20611
 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 19933 . . . . . 6 TopOn
21ad2antrr 731 . . . . 5 TopOn TopOn
3 simprl 763 . . . . . 6 TopOn TopOn
4 toponuni 19934 . . . . . . 7 TopOn
54ad2antrr 731 . . . . . 6 TopOn TopOn
63, 5sseqtrd 3501 . . . . 5 TopOn TopOn
7 eqid 2423 . . . . . 6
87clscld 20054 . . . . 5
92, 6, 8syl2anc 666 . . . 4 TopOn TopOn
10 topontop 19933 . . . . . 6 TopOn
1110ad2antlr 732 . . . . 5 TopOn TopOn
12 simprr 765 . . . . . 6 TopOn TopOn
13 toponuni 19934 . . . . . . 7 TopOn
1413ad2antlr 732 . . . . . 6 TopOn TopOn
1512, 14sseqtrd 3501 . . . . 5 TopOn TopOn
16 eqid 2423 . . . . . 6
1716clscld 20054 . . . . 5
1811, 15, 17syl2anc 666 . . . 4 TopOn TopOn
19 txcld 20610 . . . 4
209, 18, 19syl2anc 666 . . 3 TopOn TopOn
217sscls 20063 . . . . 5
222, 6, 21syl2anc 666 . . . 4 TopOn TopOn
2316sscls 20063 . . . . 5
2411, 15, 23syl2anc 666 . . . 4 TopOn TopOn
25 xpss12 4957 . . . 4
2622, 24, 25syl2anc 666 . . 3 TopOn TopOn
27 eqid 2423 . . . 4
2827clsss2 20080 . . 3
2920, 26, 28syl2anc 666 . 2 TopOn TopOn
30 relxp 4959 . . . 4
3130a1i 11 . . 3 TopOn TopOn
32 opelxp 4881 . . . 4
33 eltx 20575 . . . . . . . . 9 TopOn TopOn
3433ad2antrr 731 . . . . . . . 8 TopOn TopOn
35 eleq1 2495 . . . . . . . . . . . . 13
3635anbi1d 710 . . . . . . . . . . . 12
37362rexbidv 2947 . . . . . . . . . . 11
3837rspccva 3182 . . . . . . . . . 10
392ad2antrr 731 . . . . . . . . . . . . . . 15 TopOn TopOn
406ad2antrr 731 . . . . . . . . . . . . . . 15 TopOn TopOn
41 simplrl 769 . . . . . . . . . . . . . . 15 TopOn TopOn
42 simprll 771 . . . . . . . . . . . . . . 15 TopOn TopOn
43 simprrl 773 . . . . . . . . . . . . . . . . 17 TopOn TopOn
44 opelxp 4881 . . . . . . . . . . . . . . . . 17
4543, 44sylib 200 . . . . . . . . . . . . . . . 16 TopOn TopOn
4645simpld 461 . . . . . . . . . . . . . . 15 TopOn TopOn
477clsndisj 20083 . . . . . . . . . . . . . . 15
4839, 40, 41, 42, 46, 47syl32anc 1273 . . . . . . . . . . . . . 14 TopOn TopOn
49 n0 3772 . . . . . . . . . . . . . 14
5048, 49sylib 200 . . . . . . . . . . . . 13 TopOn TopOn
5111ad2antrr 731 . . . . . . . . . . . . . . 15 TopOn TopOn
5215ad2antrr 731 . . . . . . . . . . . . . . 15 TopOn TopOn
53 simplrr 770 . . . . . . . . . . . . . . 15 TopOn TopOn
54 simprlr 772 . . . . . . . . . . . . . . 15 TopOn TopOn
5545simprd 465 . . . . . . . . . . . . . . 15 TopOn TopOn
5616clsndisj 20083 . . . . . . . . . . . . . . 15
5751, 52, 53, 54, 55, 56syl32anc 1273 . . . . . . . . . . . . . 14 TopOn TopOn
58 n0 3772 . . . . . . . . . . . . . 14
5957, 58sylib 200 . . . . . . . . . . . . 13 TopOn TopOn
60 eeanv 2044 . . . . . . . . . . . . . 14
61 inss1 3683 . . . . . . . . . . . . . . . . . . 19
62 opelxpi 4883 . . . . . . . . . . . . . . . . . . . 20
63 inxp 4984 . . . . . . . . . . . . . . . . . . . 20
6462, 63syl6eleqr 2522 . . . . . . . . . . . . . . . . . . 19
6561, 64sseldi 3463 . . . . . . . . . . . . . . . . . 18
66 simprrr 774 . . . . . . . . . . . . . . . . . . 19 TopOn TopOn
6766sselda 3465 . . . . . . . . . . . . . . . . . 18 TopOn TopOn
6865, 67sylan2 477 . . . . . . . . . . . . . . . . 17 TopOn TopOn
69 inss2 3684 . . . . . . . . . . . . . . . . . . 19
7069, 64sseldi 3463 . . . . . . . . . . . . . . . . . 18
7170adantl 468 . . . . . . . . . . . . . . . . 17 TopOn TopOn
72 inelcm 3848 . . . . . . . . . . . . . . . . 17
7368, 71, 72syl2anc 666 . . . . . . . . . . . . . . . 16 TopOn TopOn
7473ex 436 . . . . . . . . . . . . . . 15 TopOn TopOn
7574exlimdvv 1770 . . . . . . . . . . . . . 14 TopOn TopOn
7660, 75syl5bir 222 . . . . . . . . . . . . 13 TopOn TopOn
7750, 59, 76mp2and 684 . . . . . . . . . . . 12 TopOn TopOn
7877expr 619 . . . . . . . . . . 11 TopOn TopOn
7978rexlimdvva 2925 . . . . . . . . . 10 TopOn TopOn
8038, 79syl5 34 . . . . . . . . 9 TopOn TopOn
8180expd 438 . . . . . . . 8 TopOn TopOn
8234, 81sylbid 219 . . . . . . 7 TopOn TopOn
8382ralrimiv 2838 . . . . . 6 TopOn TopOn
84 txtopon 20598 . . . . . . . . 9 TopOn TopOn TopOn
8584ad2antrr 731 . . . . . . . 8 TopOn TopOn TopOn
86 topontop 19933 . . . . . . . 8 TopOn
8785, 86syl 17 . . . . . . 7 TopOn TopOn
88 xpss12 4957 . . . . . . . . 9
8988ad2antlr 732 . . . . . . . 8 TopOn TopOn
90 toponuni 19934 . . . . . . . . 9 TopOn
9185, 90syl 17 . . . . . . . 8 TopOn TopOn
9289, 91sseqtrd 3501 . . . . . . 7 TopOn TopOn
937clsss3 20066 . . . . . . . . . . . . 13
942, 6, 93syl2anc 666 . . . . . . . . . . . 12 TopOn TopOn
9594, 5sseqtr4d 3502 . . . . . . . . . . 11 TopOn TopOn
9695sselda 3465 . . . . . . . . . 10 TopOn TopOn
9796adantrr 722 . . . . . . . . 9 TopOn TopOn
9816clsss3 20066 . . . . . . . . . . . . 13
9911, 15, 98syl2anc 666 . . . . . . . . . . . 12 TopOn TopOn
10099, 14sseqtr4d 3502 . . . . . . . . . . 11 TopOn TopOn
101100sselda 3465 . . . . . . . . . 10 TopOn TopOn
102101adantrl 721 . . . . . . . . 9 TopOn TopOn
103 opelxpi 4883 . . . . . . . . 9
10497, 102, 103syl2anc 666 . . . . . . . 8 TopOn TopOn
105104, 91eleqtrd 2513 . . . . . . 7 TopOn TopOn
10627elcls 20081 . . . . . . 7
10787, 92, 105, 106syl3anc 1265 . . . . . 6 TopOn TopOn
10883, 107mpbird 236 . . . . 5 TopOn TopOn
109108ex 436 . . . 4 TopOn TopOn
11032, 109syl5bi 221 . . 3 TopOn TopOn
11131, 110relssdv 4944 . 2 TopOn TopOn
11229, 111eqssd 3482 1 TopOn TopOn
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1438  wex 1660   wcel 1869   wne 2619  wral 2776  wrex 2777   cin 3436   wss 3437  c0 3762  cop 4003  cuni 4217   cxp 4849   wrel 4856  cfv 5599  (class class class)co 6303  ctop 19909  TopOnctopon 19910  ccld 20023  ccl 20025   ctx 20567 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-iin 4300  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-1st 6805  df-2nd 6806  df-topgen 15335  df-top 19913  df-bases 19914  df-topon 19915  df-cld 20026  df-ntr 20027  df-cls 20028  df-tx 20569 This theorem is referenced by:  clssubg  21115
 Copyright terms: Public domain W3C validator