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

Definition df-flf 21554
Description: Define a function that gives the limits of a function 𝑓 in the filter sense. (Contributed by Jeff Hankins, 14-Oct-2009.)
Assertion
Ref Expression
df-flf fLimf = (𝑥 ∈ Top, 𝑦 ran Fil ↦ (𝑓 ∈ ( 𝑥𝑚 𝑦) ↦ (𝑥 fLim (( 𝑥 FilMap 𝑓)‘𝑦))))
Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-flf
StepHypRef Expression
1 cflf 21549 . 2 class fLimf
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 ctop 20517 . . 3 class Top
5 cfil 21459 . . . . 5 class Fil
65crn 5039 . . . 4 class ran Fil
76cuni 4372 . . 3 class ran Fil
8 vf . . . 4 setvar 𝑓
92cv 1474 . . . . . 6 class 𝑥
109cuni 4372 . . . . 5 class 𝑥
113cv 1474 . . . . . 6 class 𝑦
1211cuni 4372 . . . . 5 class 𝑦
13 cmap 7744 . . . . 5 class 𝑚
1410, 12, 13co 6549 . . . 4 class ( 𝑥𝑚 𝑦)
158cv 1474 . . . . . . 7 class 𝑓
16 cfm 21547 . . . . . . 7 class FilMap
1710, 15, 16co 6549 . . . . . 6 class ( 𝑥 FilMap 𝑓)
1811, 17cfv 5804 . . . . 5 class (( 𝑥 FilMap 𝑓)‘𝑦)
19 cflim 21548 . . . . 5 class fLim
209, 18, 19co 6549 . . . 4 class (𝑥 fLim (( 𝑥 FilMap 𝑓)‘𝑦))
218, 14, 20cmpt 4643 . . 3 class (𝑓 ∈ ( 𝑥𝑚 𝑦) ↦ (𝑥 fLim (( 𝑥 FilMap 𝑓)‘𝑦)))
222, 3, 4, 7, 21cmpt2 6551 . 2 class (𝑥 ∈ Top, 𝑦 ran Fil ↦ (𝑓 ∈ ( 𝑥𝑚 𝑦) ↦ (𝑥 fLim (( 𝑥 FilMap 𝑓)‘𝑦))))
231, 22wceq 1475 1 wff fLimf = (𝑥 ∈ Top, 𝑦 ran Fil ↦ (𝑓 ∈ ( 𝑥𝑚 𝑦) ↦ (𝑥 fLim (( 𝑥 FilMap 𝑓)‘𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  flffval  21603
  Copyright terms: Public domain W3C validator