Theorem clsf2

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

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

Proof

Step	Hyp	Ref	Expression
1		clselmap.x	$$⊢X=\bigcup J$$
2		clselmap.k	$$⊢K=\mathrm{cls}\left(J\right)$$
3	1	clsf	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right):𝒫X⟶\mathrm{Clsd}\left(J\right)$$
4	2	feq1i	$$⊢K:𝒫X⟶\mathrm{Clsd}\left(J\right)\leftrightarrow \mathrm{cls}\left(J\right):𝒫X⟶\mathrm{Clsd}\left(J\right)$$
5		df-f	$$⊢K:𝒫X⟶\mathrm{Clsd}\left(J\right)\leftrightarrow \left(KFn𝒫X\wedge \mathrm{ran}K\subseteq \mathrm{Clsd}\left(J\right)\right)$$
6	4 5	sylbb1	$$⊢\mathrm{cls}\left(J\right):𝒫X⟶\mathrm{Clsd}\left(J\right)\to \left(KFn𝒫X\wedge \mathrm{ran}K\subseteq \mathrm{Clsd}\left(J\right)\right)$$
7	1	cldss2	$$⊢\mathrm{Clsd}\left(J\right)\subseteq 𝒫X$$
8		sstr2	$$⊢\mathrm{ran}K\subseteq \mathrm{Clsd}\left(J\right)\to \left(\mathrm{Clsd}\left(J\right)\subseteq 𝒫X\to \mathrm{ran}K\subseteq 𝒫X\right)$$
9	7 8	mpi	$$⊢\mathrm{ran}K\subseteq \mathrm{Clsd}\left(J\right)\to \mathrm{ran}K\subseteq 𝒫X$$
10	9	anim2i	$$⊢\left(KFn𝒫X\wedge \mathrm{ran}K\subseteq \mathrm{Clsd}\left(J\right)\right)\to \left(KFn𝒫X\wedge \mathrm{ran}K\subseteq 𝒫X\right)$$
11	3 6 10	3syl	$$⊢J\in \mathrm{Top}\to \left(KFn𝒫X\wedge \mathrm{ran}K\subseteq 𝒫X\right)$$
12		df-f	$$⊢K:𝒫X⟶𝒫X\leftrightarrow \left(KFn𝒫X\wedge \mathrm{ran}K\subseteq 𝒫X\right)$$
13	11 12	sylibr	$$⊢J\in \mathrm{Top}\to K:𝒫X⟶𝒫X$$