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

Metamath Proof Explorer

Theorem tpnei

Description: The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss . (Contributed by FL, 2-Oct-2006)

Ref Expression
Hypothesis tpnei.1 
|- X = U. J
Assertion tpnei 
|- ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )

Proof

Step Hyp Ref Expression
1 tpnei.1 
 |-  X = U. J
2 1 topopn 
 |-  ( J e. Top -> X e. J )
3 opnneiss 
 |-  ( ( J e. Top /\ X e. J /\ S C_ X ) -> X e. ( ( nei ` J ) ` S ) )
4 3 3exp 
 |-  ( J e. Top -> ( X e. J -> ( S C_ X -> X e. ( ( nei ` J ) ` S ) ) ) )
5 2 4 mpd 
 |-  ( J e. Top -> ( S C_ X -> X e. ( ( nei ` J ) ` S ) ) )
6 ssnei 
 |-  ( ( J e. Top /\ X e. ( ( nei ` J ) ` S ) ) -> S C_ X )
7 6 ex 
 |-  ( J e. Top -> ( X e. ( ( nei ` J ) ` S ) -> S C_ X ) )
8 5 7 impbid 
 |-  ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )