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 = U. J
Assertion	neisspw	|- ( J e. Top -> ( ( nei ` J ) ` S ) C_ ~P X )

Proof

Step	Hyp	Ref	Expression
1		neifval.1	|- X = U. J
2	1	neii1	|- ( ( J e. Top /\ v e. ( ( nei ` J ) ` S ) ) -> v C_ X )
3		velpw	|- ( v e. ~P X <-> v C_ X )
4	2 3	sylibr	|- ( ( J e. Top /\ v e. ( ( nei ` J ) ` S ) ) -> v e. ~P X )
5	4	ex	|- ( J e. Top -> ( v e. ( ( nei ` J ) ` S ) -> v e. ~P X ) )
6	5	ssrdv	|- ( J e. Top -> ( ( nei ` J ) ` S ) C_ ~P X )