Metamath Proof Explorer

Theorem ssnei2

Description: Any subset M of X containing a neighborhood N of a set S is a neighborhood of this set. Generalization to subsets of Property V_i of BourbakiTop1 p. I.3. (Contributed by FL, 2-Oct-2006)

Ref Expression
Hypothesis neips.1 
|- X = U. J
Assertion ssnei2 
|- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> M e. ( ( nei ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 neips.1 
 |-  X = U. J
2 simprr 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> M C_ X )
3 neii2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
4 sstr2 
 |-  ( g C_ N -> ( N C_ M -> g C_ M ) )
5 4 com12 
 |-  ( N C_ M -> ( g C_ N -> g C_ M ) )
6 5 anim2d 
 |-  ( N C_ M -> ( ( S C_ g /\ g C_ N ) -> ( S C_ g /\ g C_ M ) ) )
7 6 reximdv 
 |-  ( N C_ M -> ( E. g e. J ( S C_ g /\ g C_ N ) -> E. g e. J ( S C_ g /\ g C_ M ) ) )
8 3 7 mpan9 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ N C_ M ) -> E. g e. J ( S C_ g /\ g C_ M ) )
9 8 adantrr 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> E. g e. J ( S C_ g /\ g C_ M ) )
10 1 neiss2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ X )
11 1 isnei 
 |-  ( ( J e. Top /\ S C_ X ) -> ( M e. ( ( nei ` J ) ` S ) <-> ( M C_ X /\ E. g e. J ( S C_ g /\ g C_ M ) ) ) )
12 10 11 syldan 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( M e. ( ( nei ` J ) ` S ) <-> ( M C_ X /\ E. g e. J ( S C_ g /\ g C_ M ) ) ) )
13 12 adantr 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> ( M e. ( ( nei ` J ) ` S ) <-> ( M C_ X /\ E. g e. J ( S C_ g /\ g C_ M ) ) ) )
14 2 9 13 mpbir2and 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> M e. ( ( nei ` J ) ` S ) )