opnneiss

Description: An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007)

		Ref	Expression
	Assertion	opnneiss	$⊢ (J \in Top \land N \in J \land S \subseteq N) \to N \in nei (J) (S)$

Step	Hyp	Ref	Expression
1		simp3	$⊢ (J \in Top \land N \in J \land S \subseteq N) \to S \subseteq N$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	eltopss	$⊢ (J \in Top \land N \in J) \to N \subseteq ⋃ J$
4		sstr	$⊢ (S \subseteq N \land N \subseteq ⋃ J) \to S \subseteq ⋃ J$
5	4	ancoms	$⊢ (N \subseteq ⋃ J \land S \subseteq N) \to S \subseteq ⋃ J$
6	3 5	stoic3	$⊢ (J \in Top \land N \in J \land S \subseteq N) \to S \subseteq ⋃ J$
7	2	opnneissb	$⊢ (J \in Top \land N \in J \land S \subseteq ⋃ J) \to (S \subseteq N \leftrightarrow N \in nei (J) (S))$
8	6 7	syld3an3	$⊢ (J \in Top \land N \in J \land S \subseteq N) \to (S \subseteq N \leftrightarrow N \in nei (J) (S))$
9	1 8	mpbid	$⊢ (J \in Top \land N \in J \land S \subseteq N) \to N \in nei (J) (S)$

Metamath Proof Explorer