cldcls

Description: A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007)

		Ref	Expression
	Assertion	cldcls	$⊢ S \in Clsd (J) \to cls (J) (S) = S$

Step	Hyp	Ref	Expression
1		cldrcl	$⊢ S \in Clsd (J) \to J \in Top$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	cldss	$⊢ S \in Clsd (J) \to S \subseteq ⋃ J$
4	2	clsval	$⊢ (J \in Top \land S \subseteq ⋃ J) \to cls (J) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
5	1 3 4	syl2anc	$⊢ S \in Clsd (J) \to cls (J) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
6		intmin	$⊢ S \in Clsd (J) \to ⋂ \{x \in Clsd (J) \| S \subseteq x\} = S$
7	5 6	eqtrd	$⊢ S \in Clsd (J) \to cls (J) (S) = S$

Metamath Proof Explorer