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

Definition df-fcls 17652
Description: Define a function that takes a filter in a topology to its set of cluster points. (Contributed by Jeff Hankins, 10-Nov-2009.)
Assertion
Ref Expression
df-fcls  |-  fClus  =  ( j  e.  Top , 
f  e.  U. ran  Fil  |->  if ( U. j  =  U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `
 x ) ,  (/) ) )
Distinct variable group:    f, j, x

Detailed syntax breakdown of Definition df-fcls
StepHypRef Expression
1 cfcls 17647 . 2  class  fClus
2 vj . . 3  set  j
3 vf . . 3  set  f
4 ctop 16647 . . 3  class  Top
5 cfil 17556 . . . . 5  class  Fil
65crn 4706 . . . 4  class  ran  Fil
76cuni 3843 . . 3  class  U. ran  Fil
82cv 1631 . . . . . 6  class  j
98cuni 3843 . . . . 5  class  U. j
103cv 1631 . . . . . 6  class  f
1110cuni 3843 . . . . 5  class  U. f
129, 11wceq 1632 . . . 4  wff  U. j  =  U. f
13 vx . . . . 5  set  x
1413cv 1631 . . . . . 6  class  x
15 ccl 16771 . . . . . . 7  class  cls
168, 15cfv 5271 . . . . . 6  class  ( cls `  j )
1714, 16cfv 5271 . . . . 5  class  ( ( cls `  j ) `
 x )
1813, 10, 17ciin 3922 . . . 4  class  |^|_ x  e.  f  ( ( cls `  j ) `  x )
19 c0 3468 . . . 4  class  (/)
2012, 18, 19cif 3578 . . 3  class  if ( U. j  =  U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `  x
) ,  (/) )
212, 3, 4, 7, 20cmpt2 5876 . 2  class  ( j  e.  Top ,  f  e.  U. ran  Fil  |->  if ( U. j  = 
U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `
 x ) ,  (/) ) )
221, 21wceq 1632 1  wff  fClus  =  ( j  e.  Top , 
f  e.  U. ran  Fil  |->  if ( U. j  =  U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `
 x ) ,  (/) ) )
Colors of variables: wff set class
This definition is referenced by:  fclsval  17719  isfcls  17720
  Copyright terms: Public domain W3C validator