Definition df-fcf 21746

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

Assertion

Ref	Expression
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 ) ) ) )

Distinct variable group:   f, g, j

Detailed syntax breakdown of Definition df-fcf

Step	Hyp	Ref	Expression
1		cfcf 21741	. 2 class fClusf
2		vj	. . 3 setvar j
3		vf	. . 3 setvar f
4		ctop 20698	. . 3 class Top
5		cfil 21649	. . . . 5 class Fil
6	5	crn 5115	. . . 4 class ran Fil
7	6	cuni 4436	. . 3 class U. ran Fil
8		vg	. . . 4 setvar g
9	2	cv 1482	. . . . . 6 class j
10	9	cuni 4436	. . . . 5 class U. j
11	3	cv 1482	. . . . . 6 class f
12	11	cuni 4436	. . . . 5 class U. f
13		cmap 7857	. . . . 5 class ^m
14	10, 12, 13	co 6650	. . . 4 class ( U. j ^m U. f )
15	8	cv 1482	. . . . . . 7 class g
16		cfm 21737	. . . . . . 7 class FilMap
17	10, 15, 16	co 6650	. . . . . 6 class ( U. j FilMap g )
18	11, 17	cfv 5888	. . . . 5 class ( ( U. j FilMap g ) ` f )
19		cfcls 21740	. . . . 5 class fClus
20	9, 18, 19	co 6650	. . . 4 class ( j fClus ( ( U. j FilMap g ) ` f ) )
21	8, 14, 20	cmpt 4729	. . 3 class ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) )
22	2, 3, 4, 7, 21	cmpt2 6652	. 2 class ( j e. Top , f e. U. ran Fil |-> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) )
23	1, 22	wceq 1483	1 wff fClusf = ( j e. Top , f e. U. ran Fil |-> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) )

This definition is referenced by:  fcfval  21837