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