Theorem neii1

Description: A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007)

	Ref	Expression
Hypothesis	neifval.1	|- X = U. J
Assertion	neii1	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ X )

Proof

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