Theorem clselmap

Description: The closure function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021)

	Ref	Expression
Hypotheses	clselmap.x	$$⊢X=\bigcup J$$
	clselmap.k	$$⊢K=\mathrm{cls}\left(J\right)$$
Assertion	clselmap	$$⊢J\in \mathrm{Top}\to K\in \left({𝒫X}^{𝒫X}\right)$$

Proof

Step	Hyp	Ref	Expression
1		clselmap.x	$$⊢X=\bigcup J$$
2		clselmap.k	$$⊢K=\mathrm{cls}\left(J\right)$$
3	1 2	clsf2	$$⊢J\in \mathrm{Top}\to K:𝒫X⟶𝒫X$$
4	1	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$
5	4	pwexd	$$⊢J\in \mathrm{Top}\to 𝒫X\in \mathrm{V}$$
6	5 5	elmapd	$$⊢J\in \mathrm{Top}\to \left(K\in \left({𝒫X}^{𝒫X}\right)\leftrightarrow K:𝒫X⟶𝒫X\right)$$
7	3 6	mpbird	$$⊢J\in \mathrm{Top}\to K\in \left({𝒫X}^{𝒫X}\right)$$