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 = ( 𝑥 ∈ 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 𝑓 ) ‘ 𝑦 ) ) ) )