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

Metamath Proof Explorer

Theorem opncld

Description: The complement of an open set is closed. (Contributed by NM, 6-Oct-2006)

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

Step	Hyp	Ref	Expression
1		iscld.1	$⊢ X = ⋃ J$
2		simpr	$⊢ (J \in Top \land S \in J) \to S \in J$
3	1	eltopss	$⊢ (J \in Top \land S \in J) \to S \subseteq X$
4	1	isopn2	$⊢ (J \in Top \land S \subseteq X) \to (S \in J \leftrightarrow X ∖ S \in Clsd (J))$
5	3 4	syldan	$⊢ (J \in Top \land S \in J) \to (S \in J \leftrightarrow X ∖ S \in Clsd (J))$
6	2 5	mpbid	$⊢ (J \in Top \land S \in J) \to X ∖ S \in Clsd (J)$