Definition df-fcls 20170

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 20165	. 2 class fClus
2		vj	. . 3 setvar j
3		vf	. . 3 setvar f
4		ctop 19154	. . 3 class Top
5		cfil 20074	. . . . 5 class Fil
6	5	crn 4993	. . . 4 class ran Fil
7	6	cuni 4238	. . 3 class U. ran Fil
8	2	cv 1373	. . . . . 6 class j
9	8	cuni 4238	. . . . 5 class U. j
10	3	cv 1373	. . . . . 6 class f
11	10	cuni 4238	. . . . 5 class U. f
12	9, 11	wceq 1374	. . . 4 wff U. j = U. f
13		vx	. . . . 5 setvar x
14	13	cv 1373	. . . . . 6 class x
15		ccl 19278	. . . . . . 7 class cls
16	8, 15	cfv 5579	. . . . . 6 class ( cls ` j )
17	14, 16	cfv 5579	. . . . 5 class ( ( cls ` j ) ` x )
18	13, 10, 17	ciin 4319	. . . 4 class |^|_ x e. f ( ( cls ` j ) ` x )
19		c0 3778	. . . 4 class (/)
20	12, 18, 19	cif 3932	. . 3 class if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) )
21	2, 3, 4, 7, 20	cmpt2 6277	. 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 1374	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  20237  isfcls  20238