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 syl6bi
 |-  ( ( 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 ) )