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

Definition df-fcls 19632
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 19627 . 2  class  fClus
2 vj . . 3  setvar  j
3 vf . . 3  setvar  f
4 ctop 18616 . . 3  class  Top
5 cfil 19536 . . . . 5  class  Fil
65crn 4941 . . . 4  class  ran  Fil
76cuni 4191 . . 3  class  U. ran  Fil
82cv 1369 . . . . . 6  class  j
98cuni 4191 . . . . 5  class  U. j
103cv 1369 . . . . . 6  class  f
1110cuni 4191 . . . . 5  class  U. f
129, 11wceq 1370 . . . 4  wff  U. j  =  U. f
13 vx . . . . 5  setvar  x
1413cv 1369 . . . . . 6  class  x
15 ccl 18740 . . . . . . 7  class  cls
168, 15cfv 5518 . . . . . 6  class  ( cls `  j )
1714, 16cfv 5518 . . . . 5  class  ( ( cls `  j ) `
 x )
1813, 10, 17ciin 4272 . . . 4  class  |^|_ x  e.  f  ( ( cls `  j ) `  x )
19 c0 3737 . . . 4  class  (/)
2012, 18, 19cif 3891 . . 3  class  if ( U. j  =  U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `  x
) ,  (/) )
212, 3, 4, 7, 20cmpt2 6194 . 2  class  ( j  e.  Top ,  f  e.  U. ran  Fil  |->  if ( U. j  = 
U. f ,  |^|_ x  e.  f  ( ( cls `  j ) `
 x ) ,  (/) ) )
221, 21wceq 1370 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  19699  isfcls  19700
  Copyright terms: Public domain W3C validator