Definition df-fcf 24261

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

Assertion

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

Distinct variable group:   𝑓,𝑔,𝑗

Detailed syntax breakdown of Definition df-fcf

Step	Hyp	Ref	Expression
1		cfcf 24256	. 2 class fClusf
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		ctop 23211	. . 3 class Top
5		cfil 24164	. . . . 5 class Fil
6	5	crn 5651	. . . 4 class ran Fil
7	6	cuni 4866	. . 3 class ∪ ran Fil
8		vg	. . . 4 setvar 𝑔
9	2	cv 1568	. . . . . 6 class 𝑗
10	9	cuni 4866	. . . . 5 class ∪ 𝑗
11	3	cv 1568	. . . . . 6 class 𝑓
12	11	cuni 4866	. . . . 5 class ∪ 𝑓
13		cmap 8847	. . . . 5 class ↑m
14	10, 12, 13	co 7420	. . . 4 class (∪ 𝑗 ↑m ∪ 𝑓)
15	8	cv 1568	. . . . . . 7 class 𝑔
16		cfm 24252	. . . . . . 7 class FilMap
17	10, 15, 16	co 7420	. . . . . 6 class (∪ 𝑗 FilMap 𝑔)
18	11, 17	cfv 6538	. . . . 5 class ((∪ 𝑗 FilMap 𝑔)‘𝑓)
19		cfcls 24255	. . . . 5 class fClus
20	9, 18, 19	co 7420	. . . 4 class (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))
21	8, 14, 20	cmpt 5185	. . 3 class (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓)))
22	2, 3, 4, 7, 21	cmpo 7422	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))
23	1, 22	wceq 1569	1 wff fClusf = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))

This definition is used by:  fcfval  24352