Definition df-cld

Description: Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006)

	Ref	Expression
Assertion	df-cld	$$⊢\mathrm{Clsd}=\left(j\in \mathrm{Top}⟼\left\{x\in 𝒫\bigcup j|\bigcup j\setminus x\in j\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccld	$$class\mathrm{Clsd}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vx	$$setvarx$$
4	1	cv	$$setvarj$$
5	4	cuni	$$class\bigcup j$$
6	5	cpw	$$class𝒫\bigcup j$$
7	3	cv	$$setvarx$$
8	5 7	cdif	$$class\left(\bigcup j\setminus x\right)$$
9	8 4	wcel	$$wff\bigcup j\setminus x\in j$$
10	9 3 6	crab	$$class\left\{x\in 𝒫\bigcup j|\bigcup j\setminus x\in j\right\}$$
11	1 2 10	cmpt	$$class\left(j\in \mathrm{Top}⟼\left\{x\in 𝒫\bigcup j|\bigcup j\setminus x\in j\right\}\right)$$
12	0 11	wceq	$$wff\mathrm{Clsd}=\left(j\in \mathrm{Top}⟼\left\{x\in 𝒫\bigcup j|\bigcup j\setminus x\in j\right\}\right)$$