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 ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) ) |
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 ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) ) |