# Metamath Proof Explorer

## Theorem cldval

Description: The set of closed sets of a topology. (Note that the set of open sets is just the topology itself, so we don't have a separate definition.) (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis cldval.1 ${⊢}{X}=\bigcup {J}$
Assertion cldval ${⊢}{J}\in \mathrm{Top}\to \mathrm{Clsd}\left({J}\right)=\left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}$

### Proof

Step Hyp Ref Expression
1 cldval.1 ${⊢}{X}=\bigcup {J}$
2 1 topopn ${⊢}{J}\in \mathrm{Top}\to {X}\in {J}$
3 pwexg ${⊢}{X}\in {J}\to 𝒫{X}\in \mathrm{V}$
4 rabexg ${⊢}𝒫{X}\in \mathrm{V}\to \left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}\in \mathrm{V}$
5 2 3 4 3syl ${⊢}{J}\in \mathrm{Top}\to \left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}\in \mathrm{V}$
6 unieq ${⊢}{j}={J}\to \bigcup {j}=\bigcup {J}$
7 6 1 syl6eqr ${⊢}{j}={J}\to \bigcup {j}={X}$
8 7 pweqd ${⊢}{j}={J}\to 𝒫\bigcup {j}=𝒫{X}$
9 7 difeq1d ${⊢}{j}={J}\to \bigcup {j}\setminus {x}={X}\setminus {x}$
10 eleq12 ${⊢}\left(\bigcup {j}\setminus {x}={X}\setminus {x}\wedge {j}={J}\right)\to \left(\bigcup {j}\setminus {x}\in {j}↔{X}\setminus {x}\in {J}\right)$
11 9 10 mpancom ${⊢}{j}={J}\to \left(\bigcup {j}\setminus {x}\in {j}↔{X}\setminus {x}\in {J}\right)$
12 8 11 rabeqbidv ${⊢}{j}={J}\to \left\{{x}\in 𝒫\bigcup {j}|\bigcup {j}\setminus {x}\in {j}\right\}=\left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}$
13 df-cld ${⊢}\mathrm{Clsd}=\left({j}\in \mathrm{Top}⟼\left\{{x}\in 𝒫\bigcup {j}|\bigcup {j}\setminus {x}\in {j}\right\}\right)$
14 12 13 fvmptg ${⊢}\left({J}\in \mathrm{Top}\wedge \left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}\in \mathrm{V}\right)\to \mathrm{Clsd}\left({J}\right)=\left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}$
15 5 14 mpdan ${⊢}{J}\in \mathrm{Top}\to \mathrm{Clsd}\left({J}\right)=\left\{{x}\in 𝒫{X}|{X}\setminus {x}\in {J}\right\}$