Theorem elnei

Description: A point belongs to any of its neighborhoods. Property V_iii of BourbakiTop1 p. I.3. (Contributed by FL, 28-Sep-2006)

	Ref	Expression
Assertion	elnei	|- ( ( J e. Top /\ P e. A /\ N e. ( ( nei ` J ) ` { P } ) ) -> P e. N )

Proof

Step	Hyp	Ref	Expression
1		ssnei	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` { P } ) ) -> { P } C_ N )
2	1	3adant2	|- ( ( J e. Top /\ P e. A /\ N e. ( ( nei ` J ) ` { P } ) ) -> { P } C_ N )
3		snssg	|- ( P e. A -> ( P e. N <-> { P } C_ N ) )
4	3	3ad2ant2	|- ( ( J e. Top /\ P e. A /\ N e. ( ( nei ` J ) ` { P } ) ) -> ( P e. N <-> { P } C_ N ) )
5	2 4	mpbird	|- ( ( J e. Top /\ P e. A /\ N e. ( ( nei ` J ) ` { P } ) ) -> P e. N )