MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fcf Structured version   Visualization version   GIF version

Definition df-fcf 21793
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
StepHypRef Expression
1 cfcf 21788 . 2 class fClusf
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 ctop 20746 . . 3 class Top
5 cfil 21696 . . . . 5 class Fil
65crn 5144 . . . 4 class ran Fil
76cuni 4468 . . 3 class ran Fil
8 vg . . . 4 setvar 𝑔
92cv 1522 . . . . . 6 class 𝑗
109cuni 4468 . . . . 5 class 𝑗
113cv 1522 . . . . . 6 class 𝑓
1211cuni 4468 . . . . 5 class 𝑓
13 cmap 7899 . . . . 5 class 𝑚
1410, 12, 13co 6690 . . . 4 class ( 𝑗𝑚 𝑓)
158cv 1522 . . . . . . 7 class 𝑔
16 cfm 21784 . . . . . . 7 class FilMap
1710, 15, 16co 6690 . . . . . 6 class ( 𝑗 FilMap 𝑔)
1811, 17cfv 5926 . . . . 5 class (( 𝑗 FilMap 𝑔)‘𝑓)
19 cfcls 21787 . . . . 5 class fClus
209, 18, 19co 6690 . . . 4 class (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓))
218, 14, 20cmpt 4762 . . 3 class (𝑔 ∈ ( 𝑗𝑚 𝑓) ↦ (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓)))
222, 3, 4, 7, 21cmpt2 6692 . 2 class (𝑗 ∈ Top, 𝑓 ran Fil ↦ (𝑔 ∈ ( 𝑗𝑚 𝑓) ↦ (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓))))
231, 22wceq 1523 1 wff fClusf = (𝑗 ∈ Top, 𝑓 ran Fil ↦ (𝑔 ∈ ( 𝑗𝑚 𝑓) ↦ (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  fcfval  21884
  Copyright terms: Public domain W3C validator