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