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	$$⊢\left(J\in \mathrm{Top}\wedge N\in \mathrm{nei}\left(J\right)\left(S\right)\right)\to S\subseteq N$$

Proof

Step	Hyp	Ref	Expression
1		neii2	$$⊢\left(J\in \mathrm{Top}\wedge N\in \mathrm{nei}\left(J\right)\left(S\right)\right)\to \exists g\in J\left(S\subseteq g\wedge g\subseteq N\right)$$
2		sstr	$$⊢\left(S\subseteq g\wedge g\subseteq N\right)\to S\subseteq N$$
3	2	rexlimivw	$$⊢\exists g\in J\left(S\subseteq g\wedge g\subseteq N\right)\to S\subseteq N$$
4	1 3	syl	$$⊢\left(J\in \mathrm{Top}\wedge N\in \mathrm{nei}\left(J\right)\left(S\right)\right)\to S\subseteq N$$