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 ∈ Top ∧ S ⊆ X → S ∈ Clsd ⁡ J ↔ cls ⁡ J ⁡ S = S

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 cldcls ⊢ S ∈ Clsd ⁡ J → cls ⁡ J ⁡ S = S
3 1 clscld ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ S ∈ Clsd ⁡ J
4 eleq1 ⊢ cls ⁡ J ⁡ S = S → cls ⁡ J ⁡ S ∈ Clsd ⁡ J ↔ S ∈ Clsd ⁡ J
5 3 4 syl5ibcom ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ S = S → S ∈ Clsd ⁡ J
6 2 5 impbid2 ⊢ J ∈ Top ∧ S ⊆ X → S ∈ Clsd ⁡ J ↔ cls ⁡ J ⁡ S = S