Definition df-fcf 23001

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 22996	. 2 class fClusf
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		ctop 21950	. . 3 class Top
5		cfil 22904	. . . . 5 class Fil
6	5	crn 5581	. . . 4 class ran Fil
7	6	cuni 4836	. . 3 class ∪ ran Fil
8		vg	. . . 4 setvar 𝑔
9	2	cv 1538	. . . . . 6 class 𝑗
10	9	cuni 4836	. . . . 5 class ∪ 𝑗
11	3	cv 1538	. . . . . 6 class 𝑓
12	11	cuni 4836	. . . . 5 class ∪ 𝑓
13		cmap 8573	. . . . 5 class ↑m
14	10, 12, 13	co 7255	. . . 4 class (∪ 𝑗 ↑m ∪ 𝑓)
15	8	cv 1538	. . . . . . 7 class 𝑔
16		cfm 22992	. . . . . . 7 class FilMap
17	10, 15, 16	co 7255	. . . . . 6 class (∪ 𝑗 FilMap 𝑔)
18	11, 17	cfv 6418	. . . . 5 class ((∪ 𝑗 FilMap 𝑔)‘𝑓)
19		cfcls 22995	. . . . 5 class fClus
20	9, 18, 19	co 7255	. . . 4 class (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))
21	8, 14, 20	cmpt 5153	. . 3 class (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓)))
22	2, 3, 4, 7, 21	cmpo 7257	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))
23	1, 22	wceq 1539	1 wff fClusf = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))

This definition is referenced by:  fcfval  23092