Step |
Hyp |
Ref |
Expression |
1 |
|
simp3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑆 ⊆ 𝑁 ) |
2 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
3 |
2
|
eltopss |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ) → 𝑁 ⊆ ∪ 𝐽 ) |
4 |
|
sstr |
⊢ ( ( 𝑆 ⊆ 𝑁 ∧ 𝑁 ⊆ ∪ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 ) |
5 |
4
|
ancoms |
⊢ ( ( 𝑁 ⊆ ∪ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑆 ⊆ ∪ 𝐽 ) |
6 |
3 5
|
stoic3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑆 ⊆ ∪ 𝐽 ) |
7 |
2
|
opnneissb |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) |
8 |
6 7
|
syld3an3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → ( 𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) |
9 |
1 8
|
mpbid |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) |