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

Theorem nllyidm 17315
 Description: Idempotence of the "n-locally" predicate, i.e. being "n-locally " is a local property. (Use loclly 17313 to show 𝑛Locally 𝑛Locally 𝑛Locally .) (Contributed by Mario Carneiro, 2-Mar-2015.)
Assertion
Ref Expression
nllyidm Locally 𝑛Locally 𝑛Locally

Proof of Theorem nllyidm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 llytop 17298 . . . 4 Locally 𝑛Locally
2 llyi 17300 . . . . . . 7 Locally 𝑛Locally t 𝑛Locally
3 simprr3 1005 . . . . . . . . . . 11 Locally 𝑛Locally t 𝑛Locally t 𝑛Locally
4 simprl 732 . . . . . . . . . . . 12 Locally 𝑛Locally t 𝑛Locally
5 ssid 3273 . . . . . . . . . . . . 13
65a1i 10 . . . . . . . . . . . 12 Locally 𝑛Locally t 𝑛Locally
7 simpl1 958 . . . . . . . . . . . . . 14 Locally 𝑛Locally t 𝑛Locally Locally 𝑛Locally
87, 1syl 15 . . . . . . . . . . . . 13 Locally 𝑛Locally t 𝑛Locally
9 restopn2 17008 . . . . . . . . . . . . 13 t
108, 4, 9syl2anc 642 . . . . . . . . . . . 12 Locally 𝑛Locally t 𝑛Locally t
114, 6, 10mpbir2and 888 . . . . . . . . . . 11 Locally 𝑛Locally t 𝑛Locally t
12 simprr2 1004 . . . . . . . . . . 11 Locally 𝑛Locally t 𝑛Locally
13 nlly2i 17302 . . . . . . . . . . 11 t 𝑛Locally t t t t
143, 11, 12, 13syl3anc 1182 . . . . . . . . . 10 Locally 𝑛Locally t 𝑛Locally t t t
15 restopn2 17008 . . . . . . . . . . . . . . . 16 t
168, 4, 15syl2anc 642 . . . . . . . . . . . . . . 15 Locally 𝑛Locally t 𝑛Locally t
1716adantr 451 . . . . . . . . . . . . . 14 Locally 𝑛Locally t 𝑛Locally t
188adantr 451 . . . . . . . . . . . . . . . . . . 19 Locally 𝑛Locally t 𝑛Locally t t
19 simpr2l 1014 . . . . . . . . . . . . . . . . . . . 20 Locally 𝑛Locally t 𝑛Locally t t
20 simpr31 1045 . . . . . . . . . . . . . . . . . . . 20 Locally 𝑛Locally t 𝑛Locally t t
21 opnneip 16956 . . . . . . . . . . . . . . . . . . . 20
2218, 19, 20, 21syl3anc 1182 . . . . . . . . . . . . . . . . . . 19 Locally 𝑛Locally t 𝑛Locally t t
23 simpr32 1046 . . . . . . . . . . . . . . . . . . 19 Locally 𝑛Locally t 𝑛Locally t t
24 simpr1 961 . . . . . . . . . . . . . . . . . . . . 21 Locally 𝑛Locally t 𝑛Locally t t
25 elpwi 3709 . . . . . . . . . . . . . . . . . . . . 21
2624, 25syl 15 . . . . . . . . . . . . . . . . . . . 20 Locally 𝑛Locally t 𝑛Locally t t
274adantr 451 . . . . . . . . . . . . . . . . . . . . 21 Locally 𝑛Locally t 𝑛Locally t t
28 elssuni 3934 . . . . . . . . . . . . . . . . . . . . 21
2927, 28syl 15 . . . . . . . . . . . . . . . . . . . 20 Locally 𝑛Locally t 𝑛Locally t t
3026, 29sstrd 3265 . . . . . . . . . . . . . . . . . . 19 Locally 𝑛Locally t 𝑛Locally t t
31 eqid 2358 . . . . . . . . . . . . . . . . . . . 20
3231ssnei2 16953 . . . . . . . . . . . . . . . . . . 19
3318, 22, 23, 30, 32syl22anc 1183 . . . . . . . . . . . . . . . . . 18 Locally 𝑛Locally t 𝑛Locally t t
34 simprr1 1003 . . . . . . . . . . . . . . . . . . . . 21 Locally 𝑛Locally t 𝑛Locally
3534adantr 451 . . . . . . . . . . . . . . . . . . . 20 Locally 𝑛Locally t 𝑛Locally t t
3626, 35sstrd 3265 . . . . . . . . . . . . . . . . . . 19 Locally 𝑛Locally t 𝑛Locally t t
37 vex 2867 . . . . . . . . . . . . . . . . . . . 20
3837elpw 3707 . . . . . . . . . . . . . . . . . . 19
3936, 38sylibr 203 . . . . . . . . . . . . . . . . . 18 Locally 𝑛Locally t 𝑛Locally t t
40 elin 3434 . . . . . . . . . . . . . . . . . 18
4133, 39, 40sylanbrc 645 . . . . . . . . . . . . . . . . 17 Locally 𝑛Locally t 𝑛Locally t t
42 restabs 16996 . . . . . . . . . . . . . . . . . . 19 t t t
4318, 26, 27, 42syl3anc 1182 . . . . . . . . . . . . . . . . . 18 Locally 𝑛Locally t 𝑛Locally t t t t t
44 simpr33 1047 . . . . . . . . . . . . . . . . . 18 Locally 𝑛Locally t 𝑛Locally t t t t
4543, 44eqeltrrd 2433 . . . . . . . . . . . . . . . . 17 Locally 𝑛Locally t 𝑛Locally t t t
4641, 45jca 518 . . . . . . . . . . . . . . . 16 Locally 𝑛Locally t 𝑛Locally t t t
47463exp2 1169 . . . . . . . . . . . . . . 15 Locally 𝑛Locally t 𝑛Locally t t t
4847imp 418 . . . . . . . . . . . . . 14 Locally 𝑛Locally t 𝑛Locally t t t
4917, 48sylbid 206 . . . . . . . . . . . . 13 Locally 𝑛Locally t 𝑛Locally t t t t
5049rexlimdv 2742 . . . . . . . . . . . 12 Locally 𝑛Locally t 𝑛Locally t t t t
5150expimpd 586 . . . . . . . . . . 11 Locally 𝑛Locally t 𝑛Locally t t t t
5251reximdv2 2728 . . . . . . . . . 10 Locally 𝑛Locally t 𝑛Locally t t t t
5314, 52mpd 14 . . . . . . . . 9 Locally 𝑛Locally t 𝑛Locally t
5453expr 598 . . . . . . . 8 Locally 𝑛Locally t 𝑛Locally t
5554rexlimdva 2743 . . . . . . 7 Locally 𝑛Locally t 𝑛Locally t
562, 55mpd 14 . . . . . 6 Locally 𝑛Locally t
57563expb 1152 . . . . 5 Locally 𝑛Locally t
5857ralrimivva 2711 . . . 4 Locally 𝑛Locally t
59 isnlly 17295 . . . 4 𝑛Locally t
601, 58, 59sylanbrc 645 . . 3 Locally 𝑛Locally 𝑛Locally
6160ssriv 3260 . 2 Locally 𝑛Locally 𝑛Locally
62 nllyrest 17312 . . . . 5 𝑛Locally t 𝑛Locally
6362adantl 452 . . . 4 𝑛Locally t 𝑛Locally
64 nllytop 17299 . . . . . 6 𝑛Locally
6564ssriv 3260 . . . . 5 𝑛Locally
6665a1i 10 . . . 4 𝑛Locally
6763, 66restlly 17309 . . 3 𝑛Locally Locally 𝑛Locally
6867trud 1323 . 2 𝑛Locally Locally 𝑛Locally
6961, 68eqssi 3271 1 Locally 𝑛Locally 𝑛Locally
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wtru 1316   wceq 1642   wcel 1710  wral 2619  wrex 2620   cin 3227   wss 3228  cpw 3701  csn 3716  cuni 3906  cfv 5334  (class class class)co 5942   ↾t crest 13418  ctop 16731  cnei 16934  Locally clly 17290  𝑛Locally cnlly 17291 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-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-1st 6206  df-2nd 6207  df-recs 6472  df-rdg 6507  df-oadd 6567  df-er 6744  df-en 6949  df-fin 6952  df-fi 7252  df-rest 13420  df-topgen 13437  df-top 16736  df-bases 16738  df-topon 16739  df-nei 16935  df-lly 17292  df-nlly 17293
 Copyright terms: Public domain W3C validator