This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ X = ⋃ J
Assertion neisspw ⊢ J ∈ Top → nei ⁡ J ⁡ S ⊆ 𝒫 X

Proof

Step Hyp Ref Expression
1 neifval.1 ⊢ X = ⋃ J
2 1 neii1 ⊢ J ∈ Top ∧ v ∈ nei ⁡ J ⁡ S → v ⊆ X
3 velpw ⊢ v ∈ 𝒫 X ↔ v ⊆ X
4 2 3 sylibr ⊢ J ∈ Top ∧ v ∈ nei ⁡ J ⁡ S → v ∈ 𝒫 X
5 4 ex ⊢ J ∈ Top → v ∈ nei ⁡ J ⁡ S → v ∈ 𝒫 X
6 5 ssrdv ⊢ J ∈ Top → nei ⁡ J ⁡ S ⊆ 𝒫 X