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	eqtr4di	$$⊢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\leftrightarrow X\setminus x\in J\right)$$
11	9 10	mpancom	$$⊢j=J\to \left(\bigcup j\setminus x\in j\leftrightarrow 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\}$$