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

Metamath Proof Explorer

Theorem topcld

Description: The underlying set of a topology is closed. Part of Theorem 6.1(1) of Munkres p. 93. (Contributed by NM, 3-Oct-2006)

		Ref	Expression
	Hypothesis	iscld.1	$⊢ X = ⋃ J$
	Assertion	topcld	$⊢ J \in Top \to X \in Clsd (J)$

Step	Hyp	Ref	Expression
1		iscld.1	$⊢ X = ⋃ J$
2		difid	$⊢ X ∖ X = \emptyset$
3		0opn	$⊢ J \in Top \to \emptyset \in J$
4	2 3	eqeltrid	$⊢ J \in Top \to X ∖ X \in J$
5		ssid	$⊢ X \subseteq X$
6	4 5	jctil	$⊢ J \in Top \to (X \subseteq X \land X ∖ X \in J)$
7	1	iscld	$⊢ J \in Top \to (X \in Clsd (J) \leftrightarrow (X \subseteq X \land X ∖ X \in J))$
8	6 7	mpbird	$⊢ J \in Top \to X \in Clsd (J)$