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