Definition df-fcls

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfcls	|- fClus
1		vj	|- j
2		ctop	|- Top
3		vf	|- f
4		cfil	|- Fil
5	4	crn	|- ran Fil
6	5	cuni	|- U. ran Fil
7	1	cv	|- j
8	7	cuni	|- U. j
9	3	cv	|- f
10	9	cuni	|- U. f
11	8 10	wceq	|- U. j = U. f
12		vx	|- x
13		ccl	|- cls
14	7 13	cfv	|- ( cls ` j )
15	12	cv	|- x
16	15 14	cfv	|- ( ( cls ` j ) ` x )
17	12 9 16	ciin	|- |^|_ x e. f ( ( cls ` j ) ` x )
18		c0	|- (/)
19	11 17 18	cif	|- if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) )
20	1 3 2 6 19	cmpo	|- ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) ) )
21	0 20	wceq	|- fClus = ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) ) )