Theorem cldcls

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

	Ref	Expression
Assertion	cldcls	⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		cldrcl	⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
2		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
3	2	cldss	⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 )
4	2	clsval	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
5	1 3 4	syl2anc	⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
6		intmin	⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } = 𝑆 )
7	5 6	eqtrd	⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )