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