# Metamath Proof Explorer

## Theorem iscld4

Description: A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008)

Ref Expression
Hypothesis clscld.1 ${⊢}{X}=\bigcup {J}$
Assertion iscld4 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({S}\in \mathrm{Clsd}\left({J}\right)↔\mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {S}\right)$

### Proof

Step Hyp Ref Expression
1 clscld.1 ${⊢}{X}=\bigcup {J}$
2 1 iscld3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({S}\in \mathrm{Clsd}\left({J}\right)↔\mathrm{cls}\left({J}\right)\left({S}\right)={S}\right)$
3 1 sscls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)$
4 3 biantrud ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {S}↔\left(\mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {S}\wedge {S}\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)$
5 eqss ${⊢}\mathrm{cls}\left({J}\right)\left({S}\right)={S}↔\left(\mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {S}\wedge {S}\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
6 4 5 syl6rbbr ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\mathrm{cls}\left({J}\right)\left({S}\right)={S}↔\mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {S}\right)$
7 2 6 bitrd ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({S}\in \mathrm{Clsd}\left({J}\right)↔\mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {S}\right)$