Theorem fncld

Description: The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fncld	$$⊢\mathrm{Clsd}Fn\mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		vuniex	$$⊢\bigcup j\in \mathrm{V}$$
2	1	pwex	$$⊢𝒫\bigcup j\in \mathrm{V}$$
3	2	rabex	$$⊢\left\{x\in 𝒫\bigcup j|\bigcup j\setminus x\in j\right\}\in \mathrm{V}$$
4		df-cld	$$⊢\mathrm{Clsd}=\left(j\in \mathrm{Top}⟼\left\{x\in 𝒫\bigcup j|\bigcup j\setminus x\in j\right\}\right)$$
5	3 4	fnmpti	$$⊢\mathrm{Clsd}Fn\mathrm{Top}$$