This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cldllycmp

Description: A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest .) (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion cldllycmp ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝐴 ) ∈ 𝑛-Locally Comp )

Proof

Step Hyp Ref Expression
1 nllytop ⊢ ( 𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ Top )
2 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
3 1 2 sylan ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
4 elrest ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐽 𝑥 = ( 𝑢 ∩ 𝐴 ) ) )
5 simpll ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) → 𝐽 ∈ 𝑛-Locally Comp )
6 simprl ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) → 𝑢 ∈ 𝐽 )
7 simprr ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) → 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) )
8 7 elin1d ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) → 𝑦 ∈ 𝑢 )
9 nlly2i ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢 ) → ∃ 𝑠 ∈ 𝒫 𝑢 ∃ 𝑤 ∈ 𝐽 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) )
10 5 6 8 9 syl3anc ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) → ∃ 𝑠 ∈ 𝒫 𝑢 ∃ 𝑤 ∈ 𝐽 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) )
11 3 ad2antrr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
12 1 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝐽 ∈ Top )
13 simpllr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )
14 simprlr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑤 ∈ 𝐽 )
15 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → ( 𝑤 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
16 12 13 14 15 syl3anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑤 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
17 simprr1 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑦 ∈ 𝑤 )
18 simplrr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) )
19 18 elin2d ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑦 ∈ 𝐴 )
20 17 19 elind ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑦 ∈ ( 𝑤 ∩ 𝐴 ) )
21 opnneip ⊢ ( ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ ( 𝑤 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) ∧ 𝑦 ∈ ( 𝑤 ∩ 𝐴 ) ) → ( 𝑤 ∩ 𝐴 ) ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) )
22 11 16 20 21 syl3anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑤 ∩ 𝐴 ) ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) )
23 simprr2 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑤 ⊆ 𝑠 )
24 23 ssrind ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑤 ∩ 𝐴 ) ⊆ ( 𝑠 ∩ 𝐴 ) )
25 inss2 ⊢ ( 𝑠 ∩ 𝐴 ) ⊆ 𝐴
26 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
27 26 cldss ⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → 𝐴 ⊆ ∪ 𝐽 )
28 13 27 syl ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝐴 ⊆ ∪ 𝐽 )
29 26 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
30 12 28 29 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
31 25 30 sseqtrid ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 ∩ 𝐴 ) ⊆ ∪ ( 𝐽 ↾t 𝐴 ) )
32 eqid ⊢ ∪ ( 𝐽 ↾t 𝐴 ) = ∪ ( 𝐽 ↾t 𝐴 )
33 32 ssnei2 ⊢ ( ( ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ ( 𝑤 ∩ 𝐴 ) ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ) ∧ ( ( 𝑤 ∩ 𝐴 ) ⊆ ( 𝑠 ∩ 𝐴 ) ∧ ( 𝑠 ∩ 𝐴 ) ⊆ ∪ ( 𝐽 ↾t 𝐴 ) ) ) → ( 𝑠 ∩ 𝐴 ) ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) )
34 11 22 24 31 33 syl22anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 ∩ 𝐴 ) ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) )
35 simprll ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑠 ∈ 𝒫 𝑢 )
36 35 elpwid ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑠 ⊆ 𝑢 )
37 36 ssrind ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 ∩ 𝐴 ) ⊆ ( 𝑢 ∩ 𝐴 ) )
38 vex ⊢ 𝑠 ∈ V
39 38 inex1 ⊢ ( 𝑠 ∩ 𝐴 ) ∈ V
40 39 elpw ⊢ ( ( 𝑠 ∩ 𝐴 ) ∈ 𝒫 ( 𝑢 ∩ 𝐴 ) ↔ ( 𝑠 ∩ 𝐴 ) ⊆ ( 𝑢 ∩ 𝐴 ) )
41 37 40 sylibr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 ∩ 𝐴 ) ∈ 𝒫 ( 𝑢 ∩ 𝐴 ) )
42 34 41 elind ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 ∩ 𝐴 ) ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) )
43 25 a1i ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 ∩ 𝐴 ) ⊆ 𝐴 )
44 restabs ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑠 ∩ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐽 ↾t 𝐴 ) ↾t ( 𝑠 ∩ 𝐴 ) ) = ( 𝐽 ↾t ( 𝑠 ∩ 𝐴 ) ) )
45 12 43 13 44 syl3anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝐽 ↾t 𝐴 ) ↾t ( 𝑠 ∩ 𝐴 ) ) = ( 𝐽 ↾t ( 𝑠 ∩ 𝐴 ) ) )
46 inss1 ⊢ ( 𝑠 ∩ 𝐴 ) ⊆ 𝑠
47 46 a1i ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 ∩ 𝐴 ) ⊆ 𝑠 )
48 restabs ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑠 ∩ 𝐴 ) ⊆ 𝑠 ∧ 𝑠 ∈ 𝒫 𝑢 ) → ( ( 𝐽 ↾t 𝑠 ) ↾t ( 𝑠 ∩ 𝐴 ) ) = ( 𝐽 ↾t ( 𝑠 ∩ 𝐴 ) ) )
49 12 47 35 48 syl3anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝐽 ↾t 𝑠 ) ↾t ( 𝑠 ∩ 𝐴 ) ) = ( 𝐽 ↾t ( 𝑠 ∩ 𝐴 ) ) )
50 45 49 eqtr4d ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝐽 ↾t 𝐴 ) ↾t ( 𝑠 ∩ 𝐴 ) ) = ( ( 𝐽 ↾t 𝑠 ) ↾t ( 𝑠 ∩ 𝐴 ) ) )
51 simprr3 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝐽 ↾t 𝑠 ) ∈ Comp )
52 incom ⊢ ( 𝑠 ∩ 𝐴 ) = ( 𝐴 ∩ 𝑠 )
53 eqid ⊢ ( 𝐴 ∩ 𝑠 ) = ( 𝐴 ∩ 𝑠 )
54 ineq1 ⊢ ( 𝑣 = 𝐴 → ( 𝑣 ∩ 𝑠 ) = ( 𝐴 ∩ 𝑠 ) )
55 54 rspceeqv ⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐴 ∩ 𝑠 ) = ( 𝐴 ∩ 𝑠 ) ) → ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) ( 𝐴 ∩ 𝑠 ) = ( 𝑣 ∩ 𝑠 ) )
56 13 53 55 sylancl ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) ( 𝐴 ∩ 𝑠 ) = ( 𝑣 ∩ 𝑠 ) )
57 simplrl ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑢 ∈ 𝐽 )
58 elssuni ⊢ ( 𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽 )
59 57 58 syl ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑢 ⊆ ∪ 𝐽 )
60 36 59 sstrd ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑠 ⊆ ∪ 𝐽 )
61 26 restcld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽 ) → ( ( 𝐴 ∩ 𝑠 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑠 ) ) ↔ ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) ( 𝐴 ∩ 𝑠 ) = ( 𝑣 ∩ 𝑠 ) ) )
62 12 60 61 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝐴 ∩ 𝑠 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑠 ) ) ↔ ∃ 𝑣 ∈ ( Clsd ‘ 𝐽 ) ( 𝐴 ∩ 𝑠 ) = ( 𝑣 ∩ 𝑠 ) ) )
63 56 62 mpbird ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝐴 ∩ 𝑠 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑠 ) ) )
64 52 63 eqeltrid ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 ∩ 𝐴 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑠 ) ) )
65 cmpcld ⊢ ( ( ( 𝐽 ↾t 𝑠 ) ∈ Comp ∧ ( 𝑠 ∩ 𝐴 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑠 ) ) ) → ( ( 𝐽 ↾t 𝑠 ) ↾t ( 𝑠 ∩ 𝐴 ) ) ∈ Comp )
66 51 64 65 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝐽 ↾t 𝑠 ) ↾t ( 𝑠 ∩ 𝐴 ) ) ∈ Comp )
67 50 66 eqeltrd ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝐽 ↾t 𝐴 ) ↾t ( 𝑠 ∩ 𝐴 ) ) ∈ Comp )
68 oveq2 ⊢ ( 𝑣 = ( 𝑠 ∩ 𝐴 ) → ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) = ( ( 𝐽 ↾t 𝐴 ) ↾t ( 𝑠 ∩ 𝐴 ) ) )
69 68 eleq1d ⊢ ( 𝑣 = ( 𝑠 ∩ 𝐴 ) → ( ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ↔ ( ( 𝐽 ↾t 𝐴 ) ↾t ( 𝑠 ∩ 𝐴 ) ) ∈ Comp ) )
70 69 rspcev ⊢ ( ( ( 𝑠 ∩ 𝐴 ) ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ↾t ( 𝑠 ∩ 𝐴 ) ) ∈ Comp ) → ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp )
71 42 67 70 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) ) ) → ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp )
72 71 expr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ∧ ( 𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽 ) ) → ( ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) → ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ) )
73 72 rexlimdvva ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) → ( ∃ 𝑠 ∈ 𝒫 𝑢 ∃ 𝑤 ∈ 𝐽 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ Comp ) → ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ) )
74 10 73 mpd ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) → ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp )
75 74 anassrs ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) → ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp )
76 75 ralrimiva ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp )
77 pweq ⊢ ( 𝑥 = ( 𝑢 ∩ 𝐴 ) → 𝒫 𝑥 = 𝒫 ( 𝑢 ∩ 𝐴 ) )
78 77 ineq2d ⊢ ( 𝑥 = ( 𝑢 ∩ 𝐴 ) → ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) = ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) )
79 78 rexeqdv ⊢ ( 𝑥 = ( 𝑢 ∩ 𝐴 ) → ( ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ↔ ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ) )
80 79 raleqbi1dv ⊢ ( 𝑥 = ( 𝑢 ∩ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ↔ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 ( 𝑢 ∩ 𝐴 ) ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ) )
81 76 80 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( 𝑥 = ( 𝑢 ∩ 𝐴 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ) )
82 81 rexlimdva ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∃ 𝑢 ∈ 𝐽 𝑥 = ( 𝑢 ∩ 𝐴 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ) )
83 4 82 sylbid ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ) )
84 83 ralrimiv ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ∀ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp )
85 isnlly ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ 𝑛-Locally Comp ↔ ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ ∀ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐴 ) ↾t 𝑣 ) ∈ Comp ) )
86 3 84 85 sylanbrc ⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝐴 ) ∈ 𝑛-Locally Comp )