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

Definition df-flf 17635
Description: Define a function that gives the limits of a function  f in the filter sense. (Contributed by Jeff Hankins, 14-Oct-2009.)
Assertion
Ref Expression
df-flf  |-  fLimf  =  ( x  e.  Top , 
y  e.  U. ran  Fil  |->  ( f  e.  ( U. x  ^m  U. y )  |->  ( x 
fLim  ( ( U. x  FilMap  f ) `  y ) ) ) )
Distinct variable group:    x, f, y

Detailed syntax breakdown of Definition df-flf
StepHypRef Expression
1 cflf 17630 . 2  class  fLimf
2 vx . . 3  set  x
3 vy . . 3  set  y
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 vf . . . 4  set  f
92cv 1622 . . . . . 6  class  x
109cuni 3827 . . . . 5  class  U. x
113cv 1622 . . . . . 6  class  y
1211cuni 3827 . . . . 5  class  U. y
13 cmap 6772 . . . . 5  class  ^m
1410, 12, 13co 5858 . . . 4  class  ( U. x  ^m  U. y )
158cv 1622 . . . . . . 7  class  f
16 cfm 17628 . . . . . . 7  class  FilMap
1710, 15, 16co 5858 . . . . . 6  class  ( U. x  FilMap  f )
1811, 17cfv 5255 . . . . 5  class  ( ( U. x  FilMap  f ) `
 y )
19 cflim 17629 . . . . 5  class  fLim
209, 18, 19co 5858 . . . 4  class  ( x 
fLim  ( ( U. x  FilMap  f ) `  y ) )
218, 14, 20cmpt 4077 . . 3  class  ( f  e.  ( U. x  ^m  U. y )  |->  ( x  fLim  ( ( U. x  FilMap  f ) `
 y ) ) )
222, 3, 4, 7, 21cmpt2 5860 . 2  class  ( x  e.  Top ,  y  e.  U. ran  Fil  |->  ( f  e.  ( U. x  ^m  U. y )  |->  ( x 
fLim  ( ( U. x  FilMap  f ) `  y ) ) ) )
231, 22wceq 1623 1  wff  fLimf  =  ( x  e.  Top , 
y  e.  U. ran  Fil  |->  ( f  e.  ( U. x  ^m  U. y )  |->  ( x 
fLim  ( ( U. x  FilMap  f ) `  y ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  flffval  17684
  Copyright terms: Public domain W3C validator