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

Definition df-flf 17964
 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-flf
StepHypRef Expression
1 cflf 17959 . 2
2 vx . . 3
3 vy . . 3
4 ctop 16950 . . 3
5 cfil 17869 . . . . 5
65crn 4871 . . . 4
76cuni 4007 . . 3
8 vf . . . 4
92cv 1651 . . . . . 6
109cuni 4007 . . . . 5
113cv 1651 . . . . . 6
1211cuni 4007 . . . . 5
13 cmap 7010 . . . . 5
1410, 12, 13co 6073 . . . 4
158cv 1651 . . . . . . 7
16 cfm 17957 . . . . . . 7
1710, 15, 16co 6073 . . . . . 6
1811, 17cfv 5446 . . . . 5
19 cflim 17958 . . . . 5
209, 18, 19co 6073 . . . 4
218, 14, 20cmpt 4258 . . 3
222, 3, 4, 7, 21cmpt2 6075 . 2
231, 22wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  flffval  18013
 Copyright terms: Public domain W3C validator