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

Definition df-fcls 20170
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 20165 . 2  class  fClus
2 vj . . 3  setvar  j
3 vf . . 3  setvar  f
4 ctop 19154 . . 3  class  Top
5 cfil 20074 . . . . 5  class  Fil
65crn 4993 . . . 4  class  ran  Fil
76cuni 4238 . . 3  class  U. ran  Fil
82cv 1373 . . . . . 6  class  j
98cuni 4238 . . . . 5  class  U. j
103cv 1373 . . . . . 6  class  f
1110cuni 4238 . . . . 5  class  U. f
129, 11wceq 1374 . . . 4  wff  U. j  =  U. f
13 vx . . . . 5  setvar  x
1413cv 1373 . . . . . 6  class  x
15 ccl 19278 . . . . . . 7  class  cls
168, 15cfv 5579 . . . . . 6  class  ( cls `  j )
1714, 16cfv 5579 . . . . 5  class  ( ( cls `  j ) `
 x )
1813, 10, 17ciin 4319 . . . 4  class  |^|_ x  e.  f  ( ( cls `  j ) `  x )
19 c0 3778 . . . 4  class  (/)
2012, 18, 19cif 3932 . . 3  class  if ( U. j  =  U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `  x
) ,  (/) )
212, 3, 4, 7, 20cmpt2 6277 . 2  class  ( j  e.  Top ,  f  e.  U. ran  Fil  |->  if ( U. j  = 
U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `
 x ) ,  (/) ) )
221, 21wceq 1374 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 setvar class
This definition is referenced by:  fclsval  20237  isfcls  20238
  Copyright terms: Public domain W3C validator