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

Definition df-flim 17634
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 17629 . 2  class  fLim
2 vj . . 3  set  j
3 vf . . 3  set  f
4 ctop 16631 . . 3  class  Top
5 cfil 17540 . . . . 5  class  Fil
65crn 4690 . . . 4  class  ran  Fil
76cuni 3827 . . 3  class  U. ran  Fil
8 vx . . . . . . . . 9  set  x
98cv 1622 . . . . . . . 8  class  x
109csn 3640 . . . . . . 7  class  { x }
112cv 1622 . . . . . . . 8  class  j
12 cnei 16834 . . . . . . . 8  class  nei
1311, 12cfv 5255 . . . . . . 7  class  ( nei `  j )
1410, 13cfv 5255 . . . . . 6  class  ( ( nei `  j ) `
 { x }
)
153cv 1622 . . . . . 6  class  f
1614, 15wss 3152 . . . . 5  wff  ( ( nei `  j ) `
 { x }
)  C_  f
1711cuni 3827 . . . . . . 7  class  U. j
1817cpw 3625 . . . . . 6  class  ~P U. j
1915, 18wss 3152 . . . . 5  wff  f  C_  ~P U. j
2016, 19wa 358 . . . 4  wff  ( ( ( nei `  j
) `  { x } )  C_  f  /\  f  C_  ~P U. j )
2120, 8, 17crab 2547 . . 3  class  { x  e.  U. j  |  ( ( ( nei `  j
) `  { x } )  C_  f  /\  f  C_  ~P U. j ) }
222, 3, 4, 7, 21cmpt2 5860 . 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 1623 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  17658  elflim2  17659
  Copyright terms: Public domain W3C validator