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 = x ∈ Top , y ∈ ⋃ ran ⁡ Fil ⟼ f ∈ ⋃ x ⋃ y ⟼ x fLim ⋃ x FilMap f ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cflf class fLimf
1 vx setvar x
2 ctop class Top
3 vy setvar y
4 cfil class Fil
5 4 crn class ran ⁡ Fil
6 5 cuni class ⋃ ran ⁡ Fil
7 vf setvar f
8 1 cv setvar x
9 8 cuni class ⋃ x
10 cmap class ↑ 𝑚
11 3 cv setvar y
12 11 cuni class ⋃ y
13 9 12 10 co class ⋃ x ⋃ y
14 cflim class fLim
15 cfm class FilMap
16 7 cv setvar f
17 9 16 15 co class ⋃ x FilMap f
18 11 17 cfv class ⋃ x FilMap f ⁡ y
19 8 18 14 co class x fLim ⋃ x FilMap f ⁡ y
20 7 13 19 cmpt class f ∈ ⋃ x ⋃ y ⟼ x fLim ⋃ x FilMap f ⁡ y
21 1 3 2 6 20 cmpo class x ∈ Top , y ∈ ⋃ ran ⁡ Fil ⟼ f ∈ ⋃ x ⋃ y ⟼ x fLim ⋃ x FilMap f ⁡ y
22 0 21 wceq wff fLimf = x ∈ Top , y ∈ ⋃ ran ⁡ Fil ⟼ f ∈ ⋃ x ⋃ y ⟼ x fLim ⋃ x FilMap f ⁡ y