Definition df-fcf 21746

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 ↦ (𝑔 ∈ (∪ 𝑗 ↑𝑚 ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))

Distinct variable group:   𝑓,𝑔,𝑗

Detailed syntax breakdown of Definition df-fcf

Step	Hyp	Ref	Expression
1		cfcf 21741	. 2 class fClusf
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		ctop 20698	. . 3 class Top
5		cfil 21649	. . . . 5 class Fil
6	5	crn 5115	. . . 4 class ran Fil
7	6	cuni 4436	. . 3 class ∪ ran Fil
8		vg	. . . 4 setvar 𝑔
9	2	cv 1482	. . . . . 6 class 𝑗
10	9	cuni 4436	. . . . 5 class ∪ 𝑗
11	3	cv 1482	. . . . . 6 class 𝑓
12	11	cuni 4436	. . . . 5 class ∪ 𝑓
13		cmap 7857	. . . . 5 class ↑𝑚
14	10, 12, 13	co 6650	. . . 4 class (∪ 𝑗 ↑𝑚 ∪ 𝑓)
15	8	cv 1482	. . . . . . 7 class 𝑔
16		cfm 21737	. . . . . . 7 class FilMap
17	10, 15, 16	co 6650	. . . . . 6 class (∪ 𝑗 FilMap 𝑔)
18	11, 17	cfv 5888	. . . . 5 class ((∪ 𝑗 FilMap 𝑔)‘𝑓)
19		cfcls 21740	. . . . 5 class fClus
20	9, 18, 19	co 6650	. . . 4 class (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))
21	8, 14, 20	cmpt 4729	. . 3 class (𝑔 ∈ (∪ 𝑗 ↑𝑚 ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓)))
22	2, 3, 4, 7, 21	cmpt2 6652	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑𝑚 ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))
23	1, 22	wceq 1483	1 wff fClusf = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑𝑚 ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))

This definition is referenced by:  fcfval  21837