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 ) ) ) )