Metamath Proof Explorer

Theorem nllyrest

Description: An open subspace of an n-locally A space is also n-locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion nllyrest ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐵 ) ∈ 𝑛-Locally 𝐴 )

Proof

Step Hyp Ref Expression
1 nllytop ⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top )
2 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐵 ) ∈ Top )
3 1 2 sylan ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐵 ) ∈ Top )
4 restopn2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ) )
5 1 4 sylan ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ) )
6 simp1l ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝐽 ∈ 𝑛-Locally 𝐴 )
7 simp2l ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ 𝐽 )
8 simp3 ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
9 nlly2i ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑠 ∈ 𝒫 𝑥 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑠 ∈ 𝒫 𝑥 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) )
11 3 3ad2ant1 ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐽 ↾t 𝐵 ) ∈ Top )
12 11 3ad2ant1 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t 𝐵 ) ∈ Top )
13 simp3l ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝐽 )
14 simp3r2 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑢 ⊆ 𝑠 )
15 simp2 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ 𝒫 𝑥 )
16 15 elpwid ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ⊆ 𝑥 )
17 simp12r ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ⊆ 𝐵 )
18 16 17 sstrd ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ⊆ 𝐵 )
19 14 18 sstrd ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑢 ⊆ 𝐵 )
20 6 3ad2ant1 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ 𝑛-Locally 𝐴 )
21 20 1 syl ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top )
22 simp11r ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐵 ∈ 𝐽 )
23 restopn2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝐽 ) → ( 𝑢 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ( 𝑢 ∈ 𝐽 ∧ 𝑢 ⊆ 𝐵 ) ) )
24 21 22 23 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑢 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ( 𝑢 ∈ 𝐽 ∧ 𝑢 ⊆ 𝐵 ) ) )
25 13 19 24 mpbir2and ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ ( 𝐽 ↾t 𝐵 ) )
26 simp3r1 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ 𝑢 )
27 opnneip ⊢ ( ( ( 𝐽 ↾t 𝐵 ) ∈ Top ∧ 𝑢 ∈ ( 𝐽 ↾t 𝐵 ) ∧ 𝑦 ∈ 𝑢 ) → 𝑢 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) )
28 12 25 26 27 syl3anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) )
29 elssuni ⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ ∪ 𝐽 )
30 22 29 syl ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐵 ⊆ ∪ 𝐽 )
31 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
32 31 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ ∪ 𝐽 ) → 𝐵 = ∪ ( 𝐽 ↾t 𝐵 ) )
33 21 30 32 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐵 = ∪ ( 𝐽 ↾t 𝐵 ) )
34 18 33 sseqtrd ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ⊆ ∪ ( 𝐽 ↾t 𝐵 ) )
35 eqid ⊢ ∪ ( 𝐽 ↾t 𝐵 ) = ∪ ( 𝐽 ↾t 𝐵 )
36 35 ssnei2 ⊢ ( ( ( ( 𝐽 ↾t 𝐵 ) ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ) ∧ ( 𝑢 ⊆ 𝑠 ∧ 𝑠 ⊆ ∪ ( 𝐽 ↾t 𝐵 ) ) ) → 𝑠 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) )
37 12 28 14 34 36 syl22anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) )
38 37 15 elind ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) )
39 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽 ) → ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) = ( 𝐽 ↾t 𝑠 ) )
40 21 18 22 39 syl3anc ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) = ( 𝐽 ↾t 𝑠 ) )
41 simp3r3 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 )
42 40 41 eqeltrd ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 )
43 38 42 jca ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 ) )
44 43 3expa ⊢ ( ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 ) )
45 44 rexlimdvaa ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑠 ∈ 𝒫 𝑥 ) → ( ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) → ( 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 ) ) )
46 45 expimpd ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑠 ∈ 𝒫 𝑥 ∧ ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) → ( 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 ) ) )
47 46 reximdv2 ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑠 ∈ 𝒫 𝑥 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) → ∃ 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 ) )
48 10 47 mpd ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 )
49 48 3expa ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 )
50 49 ralrimiva ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 )
51 50 ex ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 ) )
52 5 51 sylbid ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 ) )
53 52 ralrimiv ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ∀ 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 )
54 isnlly ⊢ ( ( 𝐽 ↾t 𝐵 ) ∈ 𝑛-Locally 𝐴 ↔ ( ( 𝐽 ↾t 𝐵 ) ∈ Top ∧ ∀ 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑠 ∈ ( ( ( nei ‘ ( 𝐽 ↾t 𝐵 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑠 ) ∈ 𝐴 ) )
55 3 53 54 sylanbrc ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐵 ) ∈ 𝑛-Locally 𝐴 )