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 \in Top, y \in ⋃ ran Fil ⟼ (f \in ({⋃ x}^{⋃ y}) ⟼ x fLim (⋃ x FilMap f) (y)))$

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 \in ({⋃ x}^{⋃ y}) ⟼ x fLim (⋃ x FilMap f) (y))$
21	1 3 2 6 20	cmpo	$class (x \in Top, y \in ⋃ ran Fil ⟼ (f \in ({⋃ x}^{⋃ y}) ⟼ x fLim (⋃ x FilMap f) (y)))$
22	0 21	wceq	$wff fLimf = (x \in Top, y \in ⋃ ran Fil ⟼ (f \in ({⋃ x}^{⋃ y}) ⟼ x fLim (⋃ x FilMap f) (y)))$

Metamath Proof Explorer