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

Definition df-flim 17959
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 17954 . 2  class  fLim
2 vj . . 3  set  j
3 vf . . 3  set  f
4 ctop 16946 . . 3  class  Top
5 cfil 17865 . . . . 5  class  Fil
65crn 4870 . . . 4  class  ran  Fil
76cuni 4007 . . 3  class  U. ran  Fil
8 vx . . . . . . . . 9  set  x
98cv 1651 . . . . . . . 8  class  x
109csn 3806 . . . . . . 7  class  { x }
112cv 1651 . . . . . . . 8  class  j
12 cnei 17149 . . . . . . . 8  class  nei
1311, 12cfv 5445 . . . . . . 7  class  ( nei `  j )
1410, 13cfv 5445 . . . . . 6  class  ( ( nei `  j ) `
 { x }
)
153cv 1651 . . . . . 6  class  f
1614, 15wss 3312 . . . . 5  wff  ( ( nei `  j ) `
 { x }
)  C_  f
1711cuni 4007 . . . . . . 7  class  U. j
1817cpw 3791 . . . . . 6  class  ~P U. j
1915, 18wss 3312 . . . . 5  wff  f  C_  ~P U. j
2016, 19wa 359 . . . 4  wff  ( ( ( nei `  j
) `  { x } )  C_  f  /\  f  C_  ~P U. j )
2120, 8, 17crab 2701 . . 3  class  { x  e.  U. j  |  ( ( ( nei `  j
) `  { x } )  C_  f  /\  f  C_  ~P U. j ) }
222, 3, 4, 7, 21cmpt2 6074 . 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 1652 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  17983  elflim2  17984
  Copyright terms: Public domain W3C validator