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=\bigcup J$$
Assertion	neisspw	$$⊢J\in \mathrm{Top}\to \mathrm{nei}\left(J\right)\left(S\right)\subseteq 𝒫X$$

Proof

Step	Hyp	Ref	Expression
1		neifval.1	$$⊢X=\bigcup J$$
2	1	neii1	$$⊢\left(J\in \mathrm{Top}\wedge v\in \mathrm{nei}\left(J\right)\left(S\right)\right)\to v\subseteq X$$
3		velpw	$$⊢v\in 𝒫X\leftrightarrow v\subseteq X$$
4	2 3	sylibr	$$⊢\left(J\in \mathrm{Top}\wedge v\in \mathrm{nei}\left(J\right)\left(S\right)\right)\to v\in 𝒫X$$
5	4	ex	$$⊢J\in \mathrm{Top}\to \left(v\in \mathrm{nei}\left(J\right)\left(S\right)\to v\in 𝒫X\right)$$
6	5	ssrdv	$$⊢J\in \mathrm{Top}\to \mathrm{nei}\left(J\right)\left(S\right)\subseteq 𝒫X$$