Metamath Proof Explorer


Theorem neisspw

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 ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 )

Proof

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 ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 )