Definition df-fcls 21011

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

Assertion

Ref	Expression
df-fcls	|- fClus = ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) ) )

Distinct variable group:   f, j, x

Detailed syntax breakdown of Definition df-fcls

Step	Hyp	Ref	Expression
1		cfcls 21006	. 2 class fClus
2		vj	. . 3 setvar j
3		vf	. . 3 setvar f
4		ctop 19972	. . 3 class Top
5		cfil 20915	. . . . 5 class Fil
6	5	crn 4857	. . . 4 class ran Fil
7	6	cuni 4212	. . 3 class U. ran Fil
8	2	cv 1454	. . . . . 6 class j
9	8	cuni 4212	. . . . 5 class U. j
10	3	cv 1454	. . . . . 6 class f
11	10	cuni 4212	. . . . 5 class U. f
12	9, 11	wceq 1455	. . . 4 wff U. j = U. f
13		vx	. . . . 5 setvar x
14	13	cv 1454	. . . . . 6 class x
15		ccl 20088	. . . . . . 7 class cls
16	8, 15	cfv 5605	. . . . . 6 class ( cls ` j )
17	14, 16	cfv 5605	. . . . 5 class ( ( cls ` j ) ` x )
18	13, 10, 17	ciin 4293	. . . 4 class |^|_ x e. f ( ( cls ` j ) ` x )
19		c0 3743	. . . 4 class (/)
20	12, 18, 19	cif 3893	. . 3 class if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) )
21	2, 3, 4, 7, 20	cmpt2 6322	. 2 class ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) ) )
22	1, 21	wceq 1455	1 wff fClus = ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) ) )

This definition is referenced by:  fclsval  21078  isfcls  21079