Definition df-fcls

Description: Define a function that takes a filter in a topology to its set of cluster points. (Contributed by Jeff Hankins, 10-Nov-2009)

	Ref	Expression
Assertion	df-fcls	$$⊢\mathrm{fClus}=\left(j\in \mathrm{Top},f\in \bigcup \mathrm{ran}\mathrm{Fil}⟼if\left(\bigcup j=\bigcup f,\bigcap _{x\in f}\mathrm{cls}\left(j\right)\left(x\right),\varnothing \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfcls	$$class\mathrm{fClus}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vf	$$setvarf$$
4		cfil	$$class\mathrm{Fil}$$
5	4	crn	$$class\mathrm{ran}\mathrm{Fil}$$
6	5	cuni	$$class\bigcup \mathrm{ran}\mathrm{Fil}$$
7	1	cv	$$setvarj$$
8	7	cuni	$$class\bigcup j$$
9	3	cv	$$setvarf$$
10	9	cuni	$$class\bigcup f$$
11	8 10	wceq	$$wff\bigcup j=\bigcup f$$
12		vx	$$setvarx$$
13		ccl	$$class\mathrm{cls}$$
14	7 13	cfv	$$class\mathrm{cls}\left(j\right)$$
15	12	cv	$$setvarx$$
16	15 14	cfv	$$class\mathrm{cls}\left(j\right)\left(x\right)$$
17	12 9 16	ciin	$$class\bigcap _{x\in f}\mathrm{cls}\left(j\right)\left(x\right)$$
18		c0	$$class\varnothing$$
19	11 17 18	cif	$$classif\left(\bigcup j=\bigcup f,\bigcap _{x\in f}\mathrm{cls}\left(j\right)\left(x\right),\varnothing \right)$$
20	1 3 2 6 19	cmpo	$$class\left(j\in \mathrm{Top},f\in \bigcup \mathrm{ran}\mathrm{Fil}⟼if\left(\bigcup j=\bigcup f,\bigcap _{x\in f}\mathrm{cls}\left(j\right)\left(x\right),\varnothing \right)\right)$$
21	0 20	wceq	$$wff\mathrm{fClus}=\left(j\in \mathrm{Top},f\in \bigcup \mathrm{ran}\mathrm{Fil}⟼if\left(\bigcup j=\bigcup f,\bigcap _{x\in f}\mathrm{cls}\left(j\right)\left(x\right),\varnothing \right)\right)$$