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	|- fClusf = ( j e. Top , f e. U. ran Fil |-> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfcf	|- fClusf
1		vj	|- j
2		ctop	|- Top
3		vf	|- f
4		cfil	|- Fil
5	4	crn	|- ran Fil
6	5	cuni	|- U. ran Fil
7		vg	|- g
8	1	cv	|- j
9	8	cuni	|- U. j
10		cmap	|- ^m
11	3	cv	|- f
12	11	cuni	|- U. f
13	9 12 10	co	|- ( U. j ^m U. f )
14		cfcls	|- fClus
15		cfm	|- FilMap
16	7	cv	|- g
17	9 16 15	co	|- ( U. j FilMap g )
18	11 17	cfv	|- ( ( U. j FilMap g ) ` f )
19	8 18 14	co	|- ( j fClus ( ( U. j FilMap g ) ` f ) )
20	7 13 19	cmpt	|- ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) )
21	1 3 2 6 20	cmpo	|- ( j e. Top , f e. U. ran Fil |-> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) )
22	0 21	wceq	|- fClusf = ( j e. Top , f e. U. ran Fil |-> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) )