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 = 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 )