This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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