Definition df-cls

Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval . (Contributed by NM, 3-Oct-2006)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccl	$$class\mathrm{cls}$$
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		vy	$$setvary$$
8		ccld	$$class\mathrm{Clsd}$$
9	4 8	cfv	$$class\mathrm{Clsd}\left(j\right)$$
10	3	cv	$$setvarx$$
11	7	cv	$$setvary$$
12	10 11	wss	$$wffx\subseteq y$$
13	12 7 9	crab	$$class\left\{y\in \mathrm{Clsd}\left(j\right)|x\subseteq y\right\}$$
14	13	cint	$$class\bigcap \left\{y\in \mathrm{Clsd}\left(j\right)|x\subseteq y\right\}$$
15	3 6 14	cmpt	$$class\left(x\in 𝒫\bigcup j⟼\bigcap \left\{y\in \mathrm{Clsd}\left(j\right)|x\subseteq y\right\}\right)$$
16	1 2 15	cmpt	$$class\left(j\in \mathrm{Top}⟼\left(x\in 𝒫\bigcup j⟼\bigcap \left\{y\in \mathrm{Clsd}\left(j\right)|x\subseteq y\right\}\right)\right)$$
17	0 16	wceq	$$wff\mathrm{cls}=\left(j\in \mathrm{Top}⟼\left(x\in 𝒫\bigcup j⟼\bigcap \left\{y\in \mathrm{Clsd}\left(j\right)|x\subseteq y\right\}\right)\right)$$