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

Theorem txnlly 20638
 Description: If the property is preserved under topological products, then so is the property of being n-locally . (Contributed by Mario Carneiro, 13-Apr-2015.)
Hypothesis
Ref Expression
txlly.1
Assertion
Ref Expression
txnlly 𝑛Locally 𝑛Locally 𝑛Locally
Distinct variable groups:   ,,   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem txnlly
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nllytop 20474 . . 3 𝑛Locally
2 nllytop 20474 . . 3 𝑛Locally
3 txtop 20570 . . 3
41, 2, 3syl2an 479 . 2 𝑛Locally 𝑛Locally
5 eltx 20569 . . . 4 𝑛Locally 𝑛Locally
6 simpll 758 . . . . . . . . 9 𝑛Locally 𝑛Locally 𝑛Locally
7 simprll 770 . . . . . . . . 9 𝑛Locally 𝑛Locally
8 simprrl 772 . . . . . . . . . 10 𝑛Locally 𝑛Locally
9 xp1st 6833 . . . . . . . . . 10
108, 9syl 17 . . . . . . . . 9 𝑛Locally 𝑛Locally
11 nlly2i 20477 . . . . . . . . 9 𝑛Locally t
126, 7, 10, 11syl3anc 1264 . . . . . . . 8 𝑛Locally 𝑛Locally t
13 simplr 760 . . . . . . . . 9 𝑛Locally 𝑛Locally 𝑛Locally
14 simprlr 771 . . . . . . . . 9 𝑛Locally 𝑛Locally
15 xp2nd 6834 . . . . . . . . . 10
168, 15syl 17 . . . . . . . . 9 𝑛Locally 𝑛Locally
17 nlly2i 20477 . . . . . . . . 9 𝑛Locally t
1813, 14, 16, 17syl3anc 1264 . . . . . . . 8 𝑛Locally 𝑛Locally t
19 reeanv 2996 . . . . . . . . 9 t t t t
20 reeanv 2996 . . . . . . . . . . 11 t t t t
214ad3antrrr 734 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑛Locally t t
221ad2antrr 730 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally
2322ad2antrr 730 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally t t
2413, 2syl 17 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally
2524ad2antrr 730 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally t t
26 simprrl 772 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally
2726adantr 466 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally t t
28 simprrr 773 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally
2928adantr 466 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally t t
30 txopn 20603 . . . . . . . . . . . . . . . . . . 19
3123, 25, 27, 29, 30syl22anc 1265 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑛Locally t t
328ad2antrr 730 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally t t
33 1st2nd2 6840 . . . . . . . . . . . . . . . . . . . 20
3432, 33syl 17 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally t t
35 simprl1 1050 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally t t
36 simprr1 1053 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally t t
37 opelxpi 4881 . . . . . . . . . . . . . . . . . . . 20
3835, 36, 37syl2anc 665 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally t t
3934, 38eqeltrd 2510 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑛Locally t t
40 opnneip 20121 . . . . . . . . . . . . . . . . . 18
4121, 31, 39, 40syl3anc 1264 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑛Locally t t
42 simprl2 1051 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑛Locally t t
43 simprr2 1054 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑛Locally t t
44 xpss12 4955 . . . . . . . . . . . . . . . . . 18
4542, 43, 44syl2anc 665 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑛Locally t t
46 simprll 770 . . . . . . . . . . . . . . . . . . . . . 22 𝑛Locally 𝑛Locally
4746adantr 466 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑛Locally t t
4847elpwid 3989 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally t t
497ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑛Locally t t
50 elssuni 4245 . . . . . . . . . . . . . . . . . . . . 21
5149, 50syl 17 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally t t
5248, 51sstrd 3474 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally t t
53 simprlr 771 . . . . . . . . . . . . . . . . . . . . . 22 𝑛Locally 𝑛Locally
5453adantr 466 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑛Locally t t
5554elpwid 3989 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally t t
5614ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21 𝑛Locally 𝑛Locally t t
57 elssuni 4245 . . . . . . . . . . . . . . . . . . . . 21
5856, 57syl 17 . . . . . . . . . . . . . . . . . . . 20 𝑛Locally 𝑛Locally t t
5955, 58sstrd 3474 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally t t
60 xpss12 4955 . . . . . . . . . . . . . . . . . . 19
6152, 59, 60syl2anc 665 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑛Locally t t
62 eqid 2422 . . . . . . . . . . . . . . . . . . . 20
63 eqid 2422 . . . . . . . . . . . . . . . . . . . 20
6462, 63txuni 20593 . . . . . . . . . . . . . . . . . . 19
6523, 25, 64syl2anc 665 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑛Locally t t
6661, 65sseqtrd 3500 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑛Locally t t
67 eqid 2422 . . . . . . . . . . . . . . . . . 18
6867ssnei2 20118 . . . . . . . . . . . . . . . . 17
6921, 41, 45, 66, 68syl22anc 1265 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑛Locally t t
70 xpss12 4955 . . . . . . . . . . . . . . . . . . 19
7148, 55, 70syl2anc 665 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑛Locally t t
72 simprrr 773 . . . . . . . . . . . . . . . . . . 19 𝑛Locally 𝑛Locally
7372ad2antrr 730 . . . . . . . . . . . . . . . . . 18 𝑛Locally 𝑛Locally t t
7471, 73sstrd 3474 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑛Locally t t
75 vex 3084 . . . . . . . . . . . . . . . . . 18
7675elpw2 4584 . . . . . . . . . . . . . . . . 17
7774, 76sylibr 215 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑛Locally t t
7869, 77elind 3650 . . . . . . . . . . . . . . 15 𝑛Locally 𝑛Locally t t
79 txrest 20632 . . . . . . . . . . . . . . . . 17 t t t
8023, 25, 47, 54, 79syl22anc 1265 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑛Locally t t t t t
81 simprl3 1052 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑛Locally t t t
82 simprr3 1055 . . . . . . . . . . . . . . . . 17 𝑛Locally 𝑛Locally t t t
83 txlly.1 . . . . . . . . . . . . . . . . . 18
8483caovcl 6473 . . . . . . . . . . . . . . . . 17 t t t t
8581, 82, 84syl2anc 665 . . . . . . . . . . . . . . . 16 𝑛Locally 𝑛Locally t t t t
8680, 85eqeltrd 2510 . . . . . . . . . . . . . . 15 𝑛Locally 𝑛Locally t t t
87 oveq2 6309 . . . . . . . . . . . . . . . . 17 t t
8887eleq1d 2491 . . . . . . . . . . . . . . . 16 t t
8988rspcev 3182 . . . . . . . . . . . . . . 15 t t
9078, 86, 89syl2anc 665 . . . . . . . . . . . . . 14 𝑛Locally 𝑛Locally t t t
9190ex 435 . . . . . . . . . . . . 13 𝑛Locally 𝑛Locally t t t
9291anassrs 652 . . . . . . . . . . . 12 𝑛Locally 𝑛Locally t t t
9392rexlimdvva 2924 . . . . . . . . . . 11 𝑛Locally 𝑛Locally t t t
9420, 93syl5bir 221 . . . . . . . . . 10 𝑛Locally 𝑛Locally t t t
9594rexlimdvva 2924 . . . . . . . . 9 𝑛Locally 𝑛Locally t t t
9619, 95syl5bir 221 . . . . . . . 8 𝑛Locally 𝑛Locally t t t
9712, 18, 96mp2and 683 . . . . . . 7 𝑛Locally 𝑛Locally t
9897expr 618 . . . . . 6 𝑛Locally 𝑛Locally t
9998rexlimdvva 2924 . . . . 5 𝑛Locally 𝑛Locally t
10099ralimdv 2835 . . . 4 𝑛Locally 𝑛Locally t
1015, 100sylbid 218 . . 3 𝑛Locally 𝑛Locally t
102101ralrimiv 2837 . 2 𝑛Locally 𝑛Locally t
103 isnlly 20470 . 2 𝑛Locally t
1044, 102, 103sylanbrc 668 1 𝑛Locally 𝑛Locally 𝑛Locally
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437   wcel 1868  wral 2775  wrex 2776   cin 3435   wss 3436  cpw 3979  csn 3996  cop 4002  cuni 4216   cxp 4847  cfv 5597  (class class class)co 6301  c1st 6801  c2nd 6802   ↾t crest 15306  ctop 19903  cnei 20099  𝑛Locally cnlly 20466   ctx 20561 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-1st 6803  df-2nd 6804  df-rest 15308  df-topgen 15329  df-top 19907  df-bases 19908  df-topon 19909  df-nei 20100  df-nlly 20468  df-tx 20563 This theorem is referenced by:  xkohmeo  20816  cvmlift2lem13  30033
 Copyright terms: Public domain W3C validator