Step |
Hyp |
Ref |
Expression |
1 |
|
neifval.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
elfvdm |
⊢ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 ∈ dom ( nei ‘ 𝐽 ) ) |
3 |
2
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ dom ( nei ‘ 𝐽 ) ) |
4 |
1
|
neif |
⊢ ( 𝐽 ∈ Top → ( nei ‘ 𝐽 ) Fn 𝒫 𝑋 ) |
5 |
4
|
fndmd |
⊢ ( 𝐽 ∈ Top → dom ( nei ‘ 𝐽 ) = 𝒫 𝑋 ) |
6 |
5
|
eleq2d |
⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ dom ( nei ‘ 𝐽 ) ↔ 𝑆 ∈ 𝒫 𝑋 ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑆 ∈ dom ( nei ‘ 𝐽 ) ↔ 𝑆 ∈ 𝒫 𝑋 ) ) |
8 |
3 7
|
mpbid |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ 𝒫 𝑋 ) |
9 |
8
|
elpwid |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑋 ) |