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

Metamath Proof Explorer

Theorem neiss

Description: Any neighborhood of a set S is also a neighborhood of any subset R C_ S . Similar to Proposition 1 of BourbakiTop1 p. I.2. (Contributed by FL, 25-Sep-2006)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 neii1 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ U. J )
3 2 3adant3 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> N C_ U. J )
4 neii2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
5 4 3adant3 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> E. g e. J ( S C_ g /\ g C_ N ) )
6 sstr2 
 |-  ( R C_ S -> ( S C_ g -> R C_ g ) )
7 6 anim1d 
 |-  ( R C_ S -> ( ( S C_ g /\ g C_ N ) -> ( R C_ g /\ g C_ N ) ) )
8 7 reximdv 
 |-  ( R C_ S -> ( E. g e. J ( S C_ g /\ g C_ N ) -> E. g e. J ( R C_ g /\ g C_ N ) ) )
9 8 3ad2ant3 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> ( E. g e. J ( S C_ g /\ g C_ N ) -> E. g e. J ( R C_ g /\ g C_ N ) ) )
10 5 9 mpd 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> E. g e. J ( R C_ g /\ g C_ N ) )
11 simp1 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> J e. Top )
12 simp3 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> R C_ S )
13 1 neiss2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ U. J )
14 13 3adant3 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> S C_ U. J )
15 12 14 sstrd 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> R C_ U. J )
16 1 isnei 
 |-  ( ( J e. Top /\ R C_ U. J ) -> ( N e. ( ( nei ` J ) ` R ) <-> ( N C_ U. J /\ E. g e. J ( R C_ g /\ g C_ N ) ) ) )
17 11 15 16 syl2anc 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> ( N e. ( ( nei ` J ) ` R ) <-> ( N C_ U. J /\ E. g e. J ( R C_ g /\ g C_ N ) ) ) )
18 3 10 17 mpbir2and 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> N e. ( ( nei ` J ) ` R ) )