Metamath Proof Explorer

Theorem ssnei2

Description: Any subset M of X containing a neighborhood N of a set S is a neighborhood of this set. Generalization to subsets of Property V_i of BourbakiTop1 p. I.3. (Contributed by FL, 2-Oct-2006)

		Ref	Expression
	Hypothesis	neips.1	$⊢ X = ⋃ J$
	Assertion	ssnei2	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (N \subseteq M \land M \subseteq X)) \to M \in nei (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		neips.1	$⊢ X = ⋃ J$
2		simprr	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (N \subseteq M \land M \subseteq X)) \to M \subseteq X$
3		neii2	$⊢ (J \in Top \land N \in nei (J) (S)) \to \exists g \in J (S \subseteq g \land g \subseteq N)$
4		sstr2	$⊢ g \subseteq N \to (N \subseteq M \to g \subseteq M)$
5	4	com12	$⊢ N \subseteq M \to (g \subseteq N \to g \subseteq M)$
6	5	anim2d	$⊢ N \subseteq M \to ((S \subseteq g \land g \subseteq N) \to (S \subseteq g \land g \subseteq M))$
7	6	reximdv	$⊢ N \subseteq M \to (\exists g \in J (S \subseteq g \land g \subseteq N) \to \exists g \in J (S \subseteq g \land g \subseteq M))$
8	3 7	mpan9	$⊢ ((J \in Top \land N \in nei (J) (S)) \land N \subseteq M) \to \exists g \in J (S \subseteq g \land g \subseteq M)$
9	8	adantrr	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (N \subseteq M \land M \subseteq X)) \to \exists g \in J (S \subseteq g \land g \subseteq M)$
10	1	neiss2	$⊢ (J \in Top \land N \in nei (J) (S)) \to S \subseteq X$
11	1	isnei	$⊢ (J \in Top \land S \subseteq X) \to (M \in nei (J) (S) \leftrightarrow (M \subseteq X \land \exists g \in J (S \subseteq g \land g \subseteq M)))$
12	10 11	syldan	$⊢ (J \in Top \land N \in nei (J) (S)) \to (M \in nei (J) (S) \leftrightarrow (M \subseteq X \land \exists g \in J (S \subseteq g \land g \subseteq M)))$
13	12	adantr	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (N \subseteq M \land M \subseteq X)) \to (M \in nei (J) (S) \leftrightarrow (M \subseteq X \land \exists g \in J (S \subseteq g \land g \subseteq M)))$
14	2 9 13	mpbir2and	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (N \subseteq M \land M \subseteq X)) \to M \in nei (J) (S)$