Theorem opnneiss

Description: An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007)

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

Proof

Step	Hyp	Ref	Expression
1		simp3	|- ( ( J e. Top /\ N e. J /\ S C_ N ) -> S C_ N )
2		eqid	|- U. J = U. J
3	2	eltopss	|- ( ( J e. Top /\ N e. J ) -> N C_ U. J )
4		sstr	|- ( ( S C_ N /\ N C_ U. J ) -> S C_ U. J )
5	4	ancoms	|- ( ( N C_ U. J /\ S C_ N ) -> S C_ U. J )
6	3 5	stoic3	|- ( ( J e. Top /\ N e. J /\ S C_ N ) -> S C_ U. J )
7	2	opnneissb	|- ( ( J e. Top /\ N e. J /\ S C_ U. J ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )
8	6 7	syld3an3	|- ( ( J e. Top /\ N e. J /\ S C_ N ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )
9	1 8	mpbid	|- ( ( J e. Top /\ N e. J /\ S C_ N ) -> N e. ( ( nei ` J ) ` S ) )