Step |
Hyp |
Ref |
Expression |
1 |
|
nllyi |
⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) |
2 |
|
simprrl |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ⊆ 𝑈 ) |
3 |
|
velpw |
⊢ ( 𝑠 ∈ 𝒫 𝑈 ↔ 𝑠 ⊆ 𝑈 ) |
4 |
2 3
|
sylibr |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ 𝒫 𝑈 ) |
5 |
|
simpl1 |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ 𝑛-Locally 𝐴 ) |
6 |
|
nllytop |
⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top ) |
7 |
5 6
|
syl |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top ) |
8 |
|
simprl |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) |
9 |
|
neii2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ∃ 𝑢 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) |
10 |
7 8 9
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) |
11 |
|
simprl |
⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → { 𝑃 } ⊆ 𝑢 ) |
12 |
|
simpll3 |
⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → 𝑃 ∈ 𝑈 ) |
13 |
|
snssg |
⊢ ( 𝑃 ∈ 𝑈 → ( 𝑃 ∈ 𝑢 ↔ { 𝑃 } ⊆ 𝑢 ) ) |
14 |
12 13
|
syl |
⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → ( 𝑃 ∈ 𝑢 ↔ { 𝑃 } ⊆ 𝑢 ) ) |
15 |
11 14
|
mpbird |
⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → 𝑃 ∈ 𝑢 ) |
16 |
|
simprr |
⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → 𝑢 ⊆ 𝑠 ) |
17 |
|
simprrr |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) |
18 |
17
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) |
19 |
15 16 18
|
3jca |
⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) |
20 |
19
|
ex |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) → ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) |
21 |
20
|
reximdv |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( ∃ 𝑢 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) |
22 |
10 21
|
mpd |
⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) |
23 |
1 4 22
|
reximssdv |
⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑠 ∈ 𝒫 𝑈 ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) |