clsidm

Description: The closure operation is idempotent. (Contributed by NM, 2-Oct-2007)

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

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	clscld	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \in Clsd (J)$
3	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
4	1	iscld3	$⊢ (J \in Top \land cls (J) (S) \subseteq X) \to (cls (J) (S) \in Clsd (J) \leftrightarrow cls (J) (cls (J) (S)) = cls (J) (S))$
5	3 4	syldan	$⊢ (J \in Top \land S \subseteq X) \to (cls (J) (S) \in Clsd (J) \leftrightarrow cls (J) (cls (J) (S)) = cls (J) (S))$
6	2 5	mpbid	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (cls (J) (S)) = cls (J) (S)$

Metamath Proof Explorer