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

Definition df-fcf 19657
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  =  ( j  e.  Top , 
f  e.  U. ran  Fil  |->  ( g  e.  ( U. j  ^m  U. f )  |->  ( j 
fClus  ( ( U. j  FilMap  g ) `  f
) ) ) )
Distinct variable group:    f, g, j

Detailed syntax breakdown of Definition df-fcf
StepHypRef Expression
1 cfcf 19652 . 2  class  fClusf
2 vj . . 3  setvar  j
3 vf . . 3  setvar  f
4 ctop 18640 . . 3  class  Top
5 cfil 19560 . . . . 5  class  Fil
65crn 4952 . . . 4  class  ran  Fil
76cuni 4202 . . 3  class  U. ran  Fil
8 vg . . . 4  setvar  g
92cv 1369 . . . . . 6  class  j
109cuni 4202 . . . . 5  class  U. j
113cv 1369 . . . . . 6  class  f
1211cuni 4202 . . . . 5  class  U. f
13 cmap 7327 . . . . 5  class  ^m
1410, 12, 13co 6203 . . . 4  class  ( U. j  ^m  U. f )
158cv 1369 . . . . . . 7  class  g
16 cfm 19648 . . . . . . 7  class  FilMap
1710, 15, 16co 6203 . . . . . 6  class  ( U. j  FilMap  g )
1811, 17cfv 5529 . . . . 5  class  ( ( U. j  FilMap  g ) `
 f )
19 cfcls 19651 . . . . 5  class  fClus
209, 18, 19co 6203 . . . 4  class  ( j 
fClus  ( ( U. j  FilMap  g ) `  f
) )
218, 14, 20cmpt 4461 . . 3  class  ( g  e.  ( U. j  ^m  U. f )  |->  ( j  fClus  ( ( U. j  FilMap  g ) `
 f ) ) )
222, 3, 4, 7, 21cmpt2 6205 . 2  class  ( j  e.  Top ,  f  e.  U. ran  Fil  |->  ( g  e.  ( U. j  ^m  U. f )  |->  ( j 
fClus  ( ( U. j  FilMap  g ) `  f
) ) ) )
231, 22wceq 1370 1  wff  fClusf  =  ( j  e.  Top , 
f  e.  U. ran  Fil  |->  ( g  e.  ( U. j  ^m  U. f )  |->  ( j 
fClus  ( ( U. j  FilMap  g ) `  f
) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  fcfval  19748
  Copyright terms: Public domain W3C validator