# Metamath Proof Explorer

## Theorem iscld

Description: The predicate "the class S is a closed set". (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

### Proof

Step Hyp Ref Expression
1 iscld.1 ${⊢}{X}=\bigcup {J}$
2 1 cldval ${⊢}{J}\in \mathrm{Top}\to \mathrm{Clsd}\left({J}\right)=\left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}$
3 2 eleq2d ${⊢}{J}\in \mathrm{Top}\to \left({S}\in \mathrm{Clsd}\left({J}\right)↔{S}\in \left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}\right)$
4 difeq2 ${⊢}{x}={S}\to {X}\setminus {x}={X}\setminus {S}$
5 4 eleq1d ${⊢}{x}={S}\to \left({X}\setminus {x}\in {J}↔{X}\setminus {S}\in {J}\right)$
6 5 elrab ${⊢}{S}\in \left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}↔\left({S}\in 𝒫{X}\wedge {X}\setminus {S}\in {J}\right)$
7 3 6 syl6bb ${⊢}{J}\in \mathrm{Top}\to \left({S}\in \mathrm{Clsd}\left({J}\right)↔\left({S}\in 𝒫{X}\wedge {X}\setminus {S}\in {J}\right)\right)$
8 1 topopn ${⊢}{J}\in \mathrm{Top}\to {X}\in {J}$
9 elpw2g ${⊢}{X}\in {J}\to \left({S}\in 𝒫{X}↔{S}\subseteq {X}\right)$
10 8 9 syl ${⊢}{J}\in \mathrm{Top}\to \left({S}\in 𝒫{X}↔{S}\subseteq {X}\right)$
11 10 anbi1d ${⊢}{J}\in \mathrm{Top}\to \left(\left({S}\in 𝒫{X}\wedge {X}\setminus {S}\in {J}\right)↔\left({S}\subseteq {X}\wedge {X}\setminus {S}\in {J}\right)\right)$
12 7 11 bitrd ${⊢}{J}\in \mathrm{Top}\to \left({S}\in \mathrm{Clsd}\left({J}\right)↔\left({S}\subseteq {X}\wedge {X}\setminus {S}\in {J}\right)\right)$