Definition df-fcf

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

	Ref	Expression
Assertion	df-fcf	⊢ fClusf = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfcf	⊢ fClusf
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vf	⊢ 𝑓
4		cfil	⊢ Fil
5	4	crn	⊢ ran Fil
6	5	cuni	⊢ ∪ ran Fil
7		vg	⊢ 𝑔
8	1	cv	⊢ 𝑗
9	8	cuni	⊢ ∪ 𝑗
10		cmap	⊢ ↑m
11	3	cv	⊢ 𝑓
12	11	cuni	⊢ ∪ 𝑓
13	9 12 10	co	⊢ ( ∪ 𝑗 ↑m ∪ 𝑓 )
14		cfcls	⊢ fClus
15		cfm	⊢ FilMap
16	7	cv	⊢ 𝑔
17	9 16 15	co	⊢ ( ∪ 𝑗 FilMap 𝑔 )
18	11 17	cfv	⊢ ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 )
19	8 18 14	co	⊢ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) )
20	7 13 19	cmpt	⊢ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) )
21	1 3 2 6 20	cmpo	⊢ ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) )
22	0 21	wceq	⊢ fClusf = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) )