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 = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfcls	⊢ fClus
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vf	⊢ 𝑓
4		cfil	⊢ Fil
5	4	crn	⊢ ran Fil
6	5	cuni	⊢ ∪ ran Fil
7	1	cv	⊢ 𝑗
8	7	cuni	⊢ ∪ 𝑗
9	3	cv	⊢ 𝑓
10	9	cuni	⊢ ∪ 𝑓
11	8 10	wceq	⊢ ∪ 𝑗 = ∪ 𝑓
12		vx	⊢ 𝑥
13		ccl	⊢ cls
14	7 13	cfv	⊢ ( cls ‘ 𝑗 )
15	12	cv	⊢ 𝑥
16	15 14	cfv	⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑥 )
17	12 9 16	ciin	⊢ ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 )
18		c0	⊢ ∅
19	11 17 18	cif	⊢ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ )
20	1 3 2 6 19	cmpo	⊢ ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) )
21	0 20	wceq	⊢ fClus = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) )