MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  restnlly Structured version   Visualization version   GIF version

Theorem restnlly 21505
Description: If the property 𝐴 passes to open subspaces, then a space is n-locally 𝐴 iff it is locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
Hypothesis
Ref Expression
restlly.1 ((𝜑 ∧ (𝑗𝐴𝑥𝑗)) → (𝑗t 𝑥) ∈ 𝐴)
Assertion
Ref Expression
restnlly (𝜑 → 𝑛-Locally 𝐴 = Locally 𝐴)
Distinct variable groups:   𝑥,𝑗,𝐴   𝜑,𝑗,𝑥

Proof of Theorem restnlly
Dummy variables 𝑘 𝑠 𝑢 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nllytop 21496 . . . . . 6 (𝑘 ∈ 𝑛-Locally 𝐴𝑘 ∈ Top)
21adantl 467 . . . . 5 ((𝜑𝑘 ∈ 𝑛-Locally 𝐴) → 𝑘 ∈ Top)
3 nlly2i 21499 . . . . . . . . 9 ((𝑘 ∈ 𝑛-Locally 𝐴𝑦𝑘𝑢𝑦) → ∃𝑠 ∈ 𝒫 𝑦𝑥𝑘 (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))
433adant1l 1185 . . . . . . . 8 (((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) → ∃𝑠 ∈ 𝒫 𝑦𝑥𝑘 (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))
5 simprl 754 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑥𝑘)
6 simprr2 1274 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑥𝑠)
7 simplr 752 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑠 ∈ 𝒫 𝑦)
87elpwid 4310 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑠𝑦)
96, 8sstrd 3762 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑥𝑦)
10 selpw 4305 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 𝑦𝑥𝑦)
119, 10sylibr 224 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑥 ∈ 𝒫 𝑦)
125, 11elind 3949 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑥 ∈ (𝑘 ∩ 𝒫 𝑦))
13 simprr1 1272 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑢𝑥)
14 simpll1 1254 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → (𝜑𝑘 ∈ 𝑛-Locally 𝐴))
1514simprd 483 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑘 ∈ 𝑛-Locally 𝐴)
1615, 1syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑘 ∈ Top)
17 restabs 21189 . . . . . . . . . . . . . 14 ((𝑘 ∈ Top ∧ 𝑥𝑠𝑠 ∈ 𝒫 𝑦) → ((𝑘t 𝑠) ↾t 𝑥) = (𝑘t 𝑥))
1816, 6, 7, 17syl3anc 1476 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → ((𝑘t 𝑠) ↾t 𝑥) = (𝑘t 𝑥))
19 df-ss 3737 . . . . . . . . . . . . . . . 16 (𝑥𝑠 ↔ (𝑥𝑠) = 𝑥)
206, 19sylib 208 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → (𝑥𝑠) = 𝑥)
21 elrestr 16296 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ Top ∧ 𝑠 ∈ 𝒫 𝑦𝑥𝑘) → (𝑥𝑠) ∈ (𝑘t 𝑠))
2216, 7, 5, 21syl3anc 1476 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → (𝑥𝑠) ∈ (𝑘t 𝑠))
2320, 22eqeltrrd 2851 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝑥 ∈ (𝑘t 𝑠))
24 eleq2 2839 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑘t 𝑠) → (𝑥𝑗𝑥 ∈ (𝑘t 𝑠)))
25 oveq1 6802 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑘t 𝑠) → (𝑗t 𝑥) = ((𝑘t 𝑠) ↾t 𝑥))
2625eleq1d 2835 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑘t 𝑠) → ((𝑗t 𝑥) ∈ 𝐴 ↔ ((𝑘t 𝑠) ↾t 𝑥) ∈ 𝐴))
2724, 26imbi12d 333 . . . . . . . . . . . . . . 15 (𝑗 = (𝑘t 𝑠) → ((𝑥𝑗 → (𝑗t 𝑥) ∈ 𝐴) ↔ (𝑥 ∈ (𝑘t 𝑠) → ((𝑘t 𝑠) ↾t 𝑥) ∈ 𝐴)))
2814simpld 482 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → 𝜑)
29 restlly.1 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝐴𝑥𝑗)) → (𝑗t 𝑥) ∈ 𝐴)
3029expr 444 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐴) → (𝑥𝑗 → (𝑗t 𝑥) ∈ 𝐴))
3130ralrimiva 3115 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑗𝐴 (𝑥𝑗 → (𝑗t 𝑥) ∈ 𝐴))
3228, 31syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → ∀𝑗𝐴 (𝑥𝑗 → (𝑗t 𝑥) ∈ 𝐴))
33 simprr3 1276 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → (𝑘t 𝑠) ∈ 𝐴)
3427, 32, 33rspcdva 3466 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → (𝑥 ∈ (𝑘t 𝑠) → ((𝑘t 𝑠) ↾t 𝑥) ∈ 𝐴))
3523, 34mpd 15 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → ((𝑘t 𝑠) ↾t 𝑥) ∈ 𝐴)
3618, 35eqeltrrd 2851 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → (𝑘t 𝑥) ∈ 𝐴)
3712, 13, 36jca32 505 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) ∧ (𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴))) → (𝑥 ∈ (𝑘 ∩ 𝒫 𝑦) ∧ (𝑢𝑥 ∧ (𝑘t 𝑥) ∈ 𝐴)))
3837ex 397 . . . . . . . . . 10 ((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) → ((𝑥𝑘 ∧ (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴)) → (𝑥 ∈ (𝑘 ∩ 𝒫 𝑦) ∧ (𝑢𝑥 ∧ (𝑘t 𝑥) ∈ 𝐴))))
3938reximdv2 3162 . . . . . . . . 9 ((((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) ∧ 𝑠 ∈ 𝒫 𝑦) → (∃𝑥𝑘 (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴) → ∃𝑥 ∈ (𝑘 ∩ 𝒫 𝑦)(𝑢𝑥 ∧ (𝑘t 𝑥) ∈ 𝐴)))
4039rexlimdva 3179 . . . . . . . 8 (((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) → (∃𝑠 ∈ 𝒫 𝑦𝑥𝑘 (𝑢𝑥𝑥𝑠 ∧ (𝑘t 𝑠) ∈ 𝐴) → ∃𝑥 ∈ (𝑘 ∩ 𝒫 𝑦)(𝑢𝑥 ∧ (𝑘t 𝑥) ∈ 𝐴)))
414, 40mpd 15 . . . . . . 7 (((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ 𝑦𝑘𝑢𝑦) → ∃𝑥 ∈ (𝑘 ∩ 𝒫 𝑦)(𝑢𝑥 ∧ (𝑘t 𝑥) ∈ 𝐴))
42413expb 1113 . . . . . 6 (((𝜑𝑘 ∈ 𝑛-Locally 𝐴) ∧ (𝑦𝑘𝑢𝑦)) → ∃𝑥 ∈ (𝑘 ∩ 𝒫 𝑦)(𝑢𝑥 ∧ (𝑘t 𝑥) ∈ 𝐴))
4342ralrimivva 3120 . . . . 5 ((𝜑𝑘 ∈ 𝑛-Locally 𝐴) → ∀𝑦𝑘𝑢𝑦𝑥 ∈ (𝑘 ∩ 𝒫 𝑦)(𝑢𝑥 ∧ (𝑘t 𝑥) ∈ 𝐴))
44 islly 21491 . . . . 5 (𝑘 ∈ Locally 𝐴 ↔ (𝑘 ∈ Top ∧ ∀𝑦𝑘𝑢𝑦𝑥 ∈ (𝑘 ∩ 𝒫 𝑦)(𝑢𝑥 ∧ (𝑘t 𝑥) ∈ 𝐴)))
452, 43, 44sylanbrc 572 . . . 4 ((𝜑𝑘 ∈ 𝑛-Locally 𝐴) → 𝑘 ∈ Locally 𝐴)
4645ex 397 . . 3 (𝜑 → (𝑘 ∈ 𝑛-Locally 𝐴𝑘 ∈ Locally 𝐴))
4746ssrdv 3758 . 2 (𝜑 → 𝑛-Locally 𝐴 ⊆ Locally 𝐴)
48 llyssnlly 21501 . . 3 Locally 𝐴 ⊆ 𝑛-Locally 𝐴
4948a1i 11 . 2 (𝜑 → Locally 𝐴 ⊆ 𝑛-Locally 𝐴)
5047, 49eqssd 3769 1 (𝜑 → 𝑛-Locally 𝐴 = Locally 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  wrex 3062  cin 3722  wss 3723  𝒫 cpw 4298  (class class class)co 6795  t crest 16288  Topctop 20917  Locally clly 21487  𝑛-Locally cnlly 21488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-rest 16290  df-top 20918  df-nei 21122  df-lly 21489  df-nlly 21490
This theorem is referenced by:  loclly  21510  hausnlly  21516
  Copyright terms: Public domain W3C validator