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 = ( 𝑥 ∈ Top , 𝑦 ∈ ∪ ran Fil ↦ ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cflf	⊢ fLimf
1		vx	⊢ 𝑥
2		ctop	⊢ Top
3		vy	⊢ 𝑦
4		cfil	⊢ Fil
5	4	crn	⊢ ran Fil
6	5	cuni	⊢ ∪ ran Fil
7		vf	⊢ 𝑓
8	1	cv	⊢ 𝑥
9	8	cuni	⊢ ∪ 𝑥
10		cmap	⊢ ↑m
11	3	cv	⊢ 𝑦
12	11	cuni	⊢ ∪ 𝑦
13	9 12 10	co	⊢ ( ∪ 𝑥 ↑m ∪ 𝑦 )
14		cflim	⊢ fLim
15		cfm	⊢ FilMap
16	7	cv	⊢ 𝑓
17	9 16 15	co	⊢ ( ∪ 𝑥 FilMap 𝑓 )
18	11 17	cfv	⊢ ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 )
19	8 18 14	co	⊢ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) )
20	7 13 19	cmpt	⊢ ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) )
21	1 3 2 6 20	cmpo	⊢ ( 𝑥 ∈ Top , 𝑦 ∈ ∪ ran Fil ↦ ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) )
22	0 21	wceq	⊢ fLimf = ( 𝑥 ∈ Top , 𝑦 ∈ ∪ ran Fil ↦ ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) )