Metamath Proof Explorer


Definition df-flf

Description: Define a function that gives the limits of a function f in the filter sense. (Contributed by Jeff Hankins, 14-Oct-2009)

Ref Expression
Assertion 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 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cflf
 |-  fLimf
1 vx
 |-  x
2 ctop
 |-  Top
3 vy
 |-  y
4 cfil
 |-  Fil
5 4 crn
 |-  ran Fil
6 5 cuni
 |-  U. ran Fil
7 vf
 |-  f
8 1 cv
 |-  x
9 8 cuni
 |-  U. x
10 cmap
 |-  ^m
11 3 cv
 |-  y
12 11 cuni
 |-  U. y
13 9 12 10 co
 |-  ( U. x ^m U. y )
14 cflim
 |-  fLim
15 cfm
 |-  FilMap
16 7 cv
 |-  f
17 9 16 15 co
 |-  ( U. x FilMap f )
18 11 17 cfv
 |-  ( ( U. x FilMap f ) ` y )
19 8 18 14 co
 |-  ( x fLim ( ( U. x FilMap f ) ` y ) )
20 7 13 19 cmpt
 |-  ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) )
21 1 3 2 6 20 cmpo
 |-  ( x e. Top , y e. U. ran Fil |-> ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) )
22 0 21 wceq
 |-  fLimf = ( x e. Top , y e. U. ran Fil |-> ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) )