Description: The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | neifval.1 | ⊢ 𝑋 = ∪ 𝐽 | |
Assertion | neisspw | ⊢ ( 𝐽 ∈ Top → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neifval.1 | ⊢ 𝑋 = ∪ 𝐽 | |
2 | 1 | neii1 | ⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑣 ⊆ 𝑋 ) |
3 | velpw | ⊢ ( 𝑣 ∈ 𝒫 𝑋 ↔ 𝑣 ⊆ 𝑋 ) | |
4 | 2 3 | sylibr | ⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑣 ∈ 𝒫 𝑋 ) |
5 | 4 | ex | ⊢ ( 𝐽 ∈ Top → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑣 ∈ 𝒫 𝑋 ) ) |
6 | 5 | ssrdv | ⊢ ( 𝐽 ∈ Top → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 ) |