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

Definition df-fcls 20419
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 20414 . 2  class  fClus
2 vj . . 3  setvar  j
3 vf . . 3  setvar  f
4 ctop 19371 . . 3  class  Top
5 cfil 20323 . . . . 5  class  Fil
65crn 4990 . . . 4  class  ran  Fil
76cuni 4234 . . 3  class  U. ran  Fil
82cv 1382 . . . . . 6  class  j
98cuni 4234 . . . . 5  class  U. j
103cv 1382 . . . . . 6  class  f
1110cuni 4234 . . . . 5  class  U. f
129, 11wceq 1383 . . . 4  wff  U. j  =  U. f
13 vx . . . . 5  setvar  x
1413cv 1382 . . . . . 6  class  x
15 ccl 19496 . . . . . . 7  class  cls
168, 15cfv 5578 . . . . . 6  class  ( cls `  j )
1714, 16cfv 5578 . . . . 5  class  ( ( cls `  j ) `
 x )
1813, 10, 17ciin 4316 . . . 4  class  |^|_ x  e.  f  ( ( cls `  j ) `  x )
19 c0 3770 . . . 4  class  (/)
2012, 18, 19cif 3926 . . 3  class  if ( U. j  =  U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `  x
) ,  (/) )
212, 3, 4, 7, 20cmpt2 6283 . 2  class  ( j  e.  Top ,  f  e.  U. ran  Fil  |->  if ( U. j  = 
U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `
 x ) ,  (/) ) )
221, 21wceq 1383 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  20486  isfcls  20487
  Copyright terms: Public domain W3C validator