Definition df-flf 21744

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

Step	Hyp	Ref	Expression
1		cflf 21739	. 2 class fLimf
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		ctop 20698	. . 3 class Top
5		cfil 21649	. . . . 5 class Fil
6	5	crn 5115	. . . 4 class ran Fil
7	6	cuni 4436	. . 3 class ∪ ran Fil
8		vf	. . . 4 setvar 𝑓
9	2	cv 1482	. . . . . 6 class 𝑥
10	9	cuni 4436	. . . . 5 class ∪ 𝑥
11	3	cv 1482	. . . . . 6 class 𝑦
12	11	cuni 4436	. . . . 5 class ∪ 𝑦
13		cmap 7857	. . . . 5 class ↑𝑚
14	10, 12, 13	co 6650	. . . 4 class (∪ 𝑥 ↑𝑚 ∪ 𝑦)
15	8	cv 1482	. . . . . . 7 class 𝑓
16		cfm 21737	. . . . . . 7 class FilMap
17	10, 15, 16	co 6650	. . . . . 6 class (∪ 𝑥 FilMap 𝑓)
18	11, 17	cfv 5888	. . . . 5 class ((∪ 𝑥 FilMap 𝑓)‘𝑦)
19		cflim 21738	. . . . 5 class fLim
20	9, 18, 19	co 6650	. . . 4 class (𝑥 fLim ((∪ 𝑥 FilMap 𝑓)‘𝑦))
21	8, 14, 20	cmpt 4729	. . 3 class (𝑓 ∈ (∪ 𝑥 ↑𝑚 ∪ 𝑦) ↦ (𝑥 fLim ((∪ 𝑥 FilMap 𝑓)‘𝑦)))
22	2, 3, 4, 7, 21	cmpt2 6652	. 2 class (𝑥 ∈ Top, 𝑦 ∈ ∪ ran Fil ↦ (𝑓 ∈ (∪ 𝑥 ↑𝑚 ∪ 𝑦) ↦ (𝑥 fLim ((∪ 𝑥 FilMap 𝑓)‘𝑦))))
23	1, 22	wceq 1483	1 wff fLimf = (𝑥 ∈ Top, 𝑦 ∈ ∪ ran Fil ↦ (𝑓 ∈ (∪ 𝑥 ↑𝑚 ∪ 𝑦) ↦ (𝑥 fLim ((∪ 𝑥 FilMap 𝑓)‘𝑦))))

This definition is referenced by:  flffval  21793