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

Metamath Proof Explorer

Theorem topopn

Description: The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006)

		Ref	Expression
	Hypothesis	1open.1	$⊢ X = ⋃ J$
	Assertion	topopn	$⊢ J \in Top \to X \in J$

Step	Hyp	Ref	Expression
1		1open.1	$⊢ X = ⋃ J$
2		ssid	$⊢ J \subseteq J$
3		uniopn	$⊢ (J \in Top \land J \subseteq J) \to ⋃ J \in J$
4	2 3	mpan2	$⊢ J \in Top \to ⋃ J \in J$
5	1 4	eqeltrid	$⊢ J \in Top \to X \in J$