Step |
Hyp |
Ref |
Expression |
1 |
|
llytop |
⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top ) |
2 |
|
llyi |
⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) |
3 |
|
simpl1 |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Locally 𝐴 ) |
4 |
3 1
|
syl |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top ) |
5 |
|
simprl |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝐽 ) |
6 |
|
simprr2 |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ 𝑢 ) |
7 |
|
opnneip |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢 ) → 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) |
8 |
4 5 6 7
|
syl3anc |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) |
9 |
|
simprr1 |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ⊆ 𝑥 ) |
10 |
|
velpw |
⊢ ( 𝑢 ∈ 𝒫 𝑥 ↔ 𝑢 ⊆ 𝑥 ) |
11 |
9 10
|
sylibr |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝒫 𝑥 ) |
12 |
8 11
|
elind |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ) |
13 |
|
simprr3 |
⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) |
14 |
2 12 13
|
reximssdv |
⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) |
15 |
14
|
3expb |
⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) |
16 |
15
|
ralrimivva |
⊢ ( 𝐽 ∈ Locally 𝐴 → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) |
17 |
|
isnlly |
⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) |
18 |
1 16 17
|
sylanbrc |
⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ 𝑛-Locally 𝐴 ) |