This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ g ∈ ⋃ j ⋃ f ⟼ j fClus ⋃ j FilMap g ⁡ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfcf class fClusf
1 vj setvar j
2 ctop class Top
3 vf setvar f
4 cfil class Fil
5 4 crn class ran ⁡ Fil
6 5 cuni class ⋃ ran ⁡ Fil
7 vg setvar g
8 1 cv setvar j
9 8 cuni class ⋃ j
10 cmap class ↑ 𝑚
11 3 cv setvar f
12 11 cuni class ⋃ f
13 9 12 10 co class ⋃ j ⋃ f
14 cfcls class fClus
15 cfm class FilMap
16 7 cv setvar g
17 9 16 15 co class ⋃ j FilMap g
18 11 17 cfv class ⋃ j FilMap g ⁡ f
19 8 18 14 co class j fClus ⋃ j FilMap g ⁡ f
20 7 13 19 cmpt class g ∈ ⋃ j ⋃ f ⟼ j fClus ⋃ j FilMap g ⁡ f
21 1 3 2 6 20 cmpo class j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ g ∈ ⋃ j ⋃ f ⟼ j fClus ⋃ j FilMap g ⁡ f
22 0 21 wceq wff fClusf = j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ g ∈ ⋃ j ⋃ f ⟼ j fClus ⋃ j FilMap g ⁡ f