This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Top \land N \in nei (J) (S)) \to S \subseteq N$

Step	Hyp	Ref	Expression
1		neii2	$⊢ (J \in Top \land N \in nei (J) (S)) \to \exists g \in J (S \subseteq g \land g \subseteq N)$
2		sstr	$⊢ (S \subseteq g \land g \subseteq N) \to S \subseteq N$
3	2	rexlimivw	$⊢ \exists g \in J (S \subseteq g \land g \subseteq N) \to S \subseteq N$
4	1 3	syl	$⊢ (J \in Top \land N \in nei (J) (S)) \to S \subseteq N$