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 )