Metamath Proof Explorer


Theorem ssnei

Description: A set is included in any of its neighborhoods. Generalization to subsets of elnei . (Contributed by FL, 16-Nov-2006)

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

Proof

Step Hyp Ref Expression
1 neii2
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
2 sstr
 |-  ( ( S C_ g /\ g C_ N ) -> S C_ N )
3 2 rexlimivw
 |-  ( E. g e. J ( S C_ g /\ g C_ N ) -> S C_ N )
4 1 3 syl
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ N )