Metamath Proof Explorer


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