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

Definition df-fcf 17637
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 17632 . 2  class  fClusf
2 vj . . 3  set  j
3 vf . . 3  set  f
4 ctop 16631 . . 3  class  Top
5 cfil 17540 . . . . 5  class  Fil
65crn 4690 . . . 4  class  ran  Fil
76cuni 3827 . . 3  class  U. ran  Fil
8 vg . . . 4  set  g
92cv 1622 . . . . . 6  class  j
109cuni 3827 . . . . 5  class  U. j
113cv 1622 . . . . . 6  class  f
1211cuni 3827 . . . . 5  class  U. f
13 cmap 6772 . . . . 5  class  ^m
1410, 12, 13co 5858 . . . 4  class  ( U. j  ^m  U. f )
158cv 1622 . . . . . . 7  class  g
16 cfm 17628 . . . . . . 7  class  FilMap
1710, 15, 16co 5858 . . . . . 6  class  ( U. j  FilMap  g )
1811, 17cfv 5255 . . . . 5  class  ( ( U. j  FilMap  g ) `
 f )
19 cfcls 17631 . . . . 5  class  fClus
209, 18, 19co 5858 . . . 4  class  ( j 
fClus  ( ( U. j  FilMap  g ) `  f
) )
218, 14, 20cmpt 4077 . . 3  class  ( g  e.  ( U. j  ^m  U. f )  |->  ( j  fClus  ( ( U. j  FilMap  g ) `
 f ) ) )
222, 3, 4, 7, 21cmpt2 5860 . 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 1623 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 set class
This definition is referenced by:  fcfval  17728
  Copyright terms: Public domain W3C validator