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

Definition df-flim 17629
Description: Define a function (indexed by a topology  j) whose value is the limits of a filter  f. (Contributed by Jeff Hankins, 4-Sep-2009.)
Assertion
Ref Expression
df-flim  |-  fLim  =  ( j  e.  Top ,  f  e.  U. ran  Fil  |->  { x  e.  U. j  |  ( (
( nei `  j
) `  { x } )  C_  f  /\  f  C_  ~P U. j ) } )
Distinct variable group:    f, j, x

Detailed syntax breakdown of Definition df-flim
StepHypRef Expression
1 cflim 17624 . 2  class  fLim
2 vj . . 3  set  j
3 vf . . 3  set  f
4 ctop 16626 . . 3  class  Top
5 cfil 17535 . . . . 5  class  Fil
65crn 4690 . . . 4  class  ran  Fil
76cuni 3829 . . 3  class  U. ran  Fil
8 vx . . . . . . . . 9  set  x
98cv 1623 . . . . . . . 8  class  x
109csn 3642 . . . . . . 7  class  { x }
112cv 1623 . . . . . . . 8  class  j
12 cnei 16829 . . . . . . . 8  class  nei
1311, 12cfv 5222 . . . . . . 7  class  ( nei `  j )
1410, 13cfv 5222 . . . . . 6  class  ( ( nei `  j ) `
 { x }
)
153cv 1623 . . . . . 6  class  f
1614, 15wss 3154 . . . . 5  wff  ( ( nei `  j ) `
 { x }
)  C_  f
1711cuni 3829 . . . . . . 7  class  U. j
1817cpw 3627 . . . . . 6  class  ~P U. j
1915, 18wss 3154 . . . . 5  wff  f  C_  ~P U. j
2016, 19wa 360 . . . 4  wff  ( ( ( nei `  j
) `  { x } )  C_  f  /\  f  C_  ~P U. j )
2120, 8, 17crab 2549 . . 3  class  { x  e.  U. j  |  ( ( ( nei `  j
) `  { x } )  C_  f  /\  f  C_  ~P U. j ) }
222, 3, 4, 7, 21cmpt2 5822 . 2  class  ( j  e.  Top ,  f  e.  U. ran  Fil  |->  { x  e.  U. j  |  ( ( ( nei `  j ) `
 { x }
)  C_  f  /\  f  C_  ~P U. j
) } )
231, 22wceq 1624 1  wff  fLim  =  ( j  e.  Top ,  f  e.  U. ran  Fil  |->  { x  e.  U. j  |  ( (
( nei `  j
) `  { x } )  C_  f  /\  f  C_  ~P U. j ) } )
Colors of variables: wff set class
This definition is referenced by:  flimval  17653  elflim2  17654
  Copyright terms: Public domain W3C validator