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

Metamath Proof Explorer

Theorem iscld3

Description: A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	iscld3	$⊢ (J \in Top \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) = S)$

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		cldcls	$⊢ S \in Clsd (J) \to cls (J) (S) = S$
3	1	clscld	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \in Clsd (J)$
4		eleq1	$⊢ cls (J) (S) = S \to (cls (J) (S) \in Clsd (J) \leftrightarrow S \in Clsd (J))$
5	3 4	syl5ibcom	$⊢ (J \in Top \land S \subseteq X) \to (cls (J) (S) = S \to S \in Clsd (J))$
6	2 5	impbid2	$⊢ (J \in Top \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) = S)$