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 𝑋 = 𝐽
Assertion iscld3 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )

Proof

Step Hyp Ref Expression
1 clscld.1 𝑋 = 𝐽
2 cldcls ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )
3 1 clscld ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
4 eleq1 ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ↔ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) )
5 3 4 syl5ibcom ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆𝑆 ∈ ( Clsd ‘ 𝐽 ) ) )
6 2 5 impbid2 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )