Definition df-fcf

Description: Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009)

	Ref	Expression
Assertion	df-fcf	$$⊢\mathrm{fClusf}=\left(j\in \mathrm{Top},f\in \bigcup \mathrm{ran}\mathrm{Fil}⟼\left(g\in \left({\bigcup j}^{\bigcup f}\right)⟼j\mathrm{fClus}\left(\bigcup j\mathrm{FilMap}g\right)\left(f\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfcf	$$class\mathrm{fClusf}$$
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		vg	$$setvarg$$
8	1	cv	$$setvarj$$
9	8	cuni	$$class\bigcup j$$
10		cmap	$$class{\uparrow }_{𝑚}$$
11	3	cv	$$setvarf$$
12	11	cuni	$$class\bigcup f$$
13	9 12 10	co	$$class\left({\bigcup j}^{\bigcup f}\right)$$
14		cfcls	$$class\mathrm{fClus}$$
15		cfm	$$class\mathrm{FilMap}$$
16	7	cv	$$setvarg$$
17	9 16 15	co	$$class\left(\bigcup j\mathrm{FilMap}g\right)$$
18	11 17	cfv	$$class\left(\bigcup j\mathrm{FilMap}g\right)\left(f\right)$$
19	8 18 14	co	$$class\left(j\mathrm{fClus}\left(\bigcup j\mathrm{FilMap}g\right)\left(f\right)\right)$$
20	7 13 19	cmpt	$$class\left(g\in \left({\bigcup j}^{\bigcup f}\right)⟼j\mathrm{fClus}\left(\bigcup j\mathrm{FilMap}g\right)\left(f\right)\right)$$
21	1 3 2 6 20	cmpo	$$class\left(j\in \mathrm{Top},f\in \bigcup \mathrm{ran}\mathrm{Fil}⟼\left(g\in \left({\bigcup j}^{\bigcup f}\right)⟼j\mathrm{fClus}\left(\bigcup j\mathrm{FilMap}g\right)\left(f\right)\right)\right)$$
22	0 21	wceq	$$wff\mathrm{fClusf}=\left(j\in \mathrm{Top},f\in \bigcup \mathrm{ran}\mathrm{Fil}⟼\left(g\in \left({\bigcup j}^{\bigcup f}\right)⟼j\mathrm{fClus}\left(\bigcup j\mathrm{FilMap}g\right)\left(f\right)\right)\right)$$