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

Metamath Proof Explorer

Theorem neii2

Description: Property of a neighborhood. (Contributed by NM, 12-Feb-2007)

Ref Expression
Assertion neii2 
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 neiss2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ U. J )
3 1 isnei 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ U. J /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
4 simpr 
 |-  ( ( N C_ U. J /\ E. g e. J ( S C_ g /\ g C_ N ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
5 3 4 biimtrdi 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( N e. ( ( nei ` J ) ` S ) -> E. g e. J ( S C_ g /\ g C_ N ) ) )
6 5 impancom 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( S C_ U. J -> E. g e. J ( S C_ g /\ g C_ N ) ) )
7 2 6 mpd 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )