tpnei

Description: The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss . (Contributed by FL, 2-Oct-2006)

		Ref	Expression
	Hypothesis	tpnei.1	$⊢ X = ⋃ J$
	Assertion	tpnei	$⊢ J \in Top \to (S \subseteq X \leftrightarrow X \in nei (J) (S))$

Step	Hyp	Ref	Expression
1		tpnei.1	$⊢ X = ⋃ J$
2	1	topopn	$⊢ J \in Top \to X \in J$
3		opnneiss	$⊢ (J \in Top \land X \in J \land S \subseteq X) \to X \in nei (J) (S)$
4	3	3exp	$⊢ J \in Top \to (X \in J \to (S \subseteq X \to X \in nei (J) (S)))$
5	2 4	mpd	$⊢ J \in Top \to (S \subseteq X \to X \in nei (J) (S))$
6		ssnei	$⊢ (J \in Top \land X \in nei (J) (S)) \to S \subseteq X$
7	6	ex	$⊢ J \in Top \to (X \in nei (J) (S) \to S \subseteq X)$
8	5 7	impbid	$⊢ J \in Top \to (S \subseteq X \leftrightarrow X \in nei (J) (S))$

Metamath Proof Explorer