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

Definition df-flf 17630
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 17625 . 2  class  fLimf
2 vx . . 3  set  x
3 vy . . 3  set  y
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 vf . . . 4  set  f
92cv 1623 . . . . . 6  class  x
109cuni 3829 . . . . 5  class  U. x
113cv 1623 . . . . . 6  class  y
1211cuni 3829 . . . . 5  class  U. y
13 cmap 6768 . . . . 5  class  ^m
1410, 12, 13co 5820 . . . 4  class  ( U. x  ^m  U. y )
158cv 1623 . . . . . . 7  class  f
16 cfm 17623 . . . . . . 7  class  FilMap
1710, 15, 16co 5820 . . . . . 6  class  ( U. x  FilMap  f )
1811, 17cfv 5222 . . . . 5  class  ( ( U. x  FilMap  f ) `
 y )
19 cflim 17624 . . . . 5  class  fLim
209, 18, 19co 5820 . . . 4  class  ( x 
fLim  ( ( U. x  FilMap  f ) `  y ) )
218, 14, 20cmpt 4079 . . 3  class  ( f  e.  ( U. x  ^m  U. y )  |->  ( x  fLim  ( ( U. x  FilMap  f ) `
 y ) ) )
222, 3, 4, 7, 21cmpt2 5822 . 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 1624 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  17679
  Copyright terms: Public domain W3C validator