df-flim

Description: Define a function (indexed by a topology j ) whose value is the limits of a filter f . (Contributed by Jeff Hankins, 4-Sep-2009)

		Ref	Expression
	Assertion	df-flim	$⊢ fLim = (j \in Top, f \in ⋃ ran Fil ⟼ \{x \in ⋃ j \| (nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j)\})$

Step	Hyp	Ref	Expression
0		cflim	$class fLim$
1		vj	$setvar j$
2		ctop	$class Top$
3		vf	$setvar f$
4		cfil	$class Fil$
5	4	crn	$class ran Fil$
6	5	cuni	$class ⋃ ran Fil$
7		vx	$setvar x$
8	1	cv	$setvar j$
9	8	cuni	$class ⋃ j$
10		cnei	$class nei$
11	8 10	cfv	$class nei (j)$
12	7	cv	$setvar x$
13	12	csn	$class \{x\}$
14	13 11	cfv	$class nei (j) (\{x\})$
15	3	cv	$setvar f$
16	14 15	wss	$wff nei (j) (\{x\}) \subseteq f$
17	9	cpw	$class 𝒫 ⋃ j$
18	15 17	wss	$wff f \subseteq 𝒫 ⋃ j$
19	16 18	wa	$wff (nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j)$
20	19 7 9	crab	$class \{x \in ⋃ j \| (nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j)\}$
21	1 3 2 6 20	cmpo	$class (j \in Top, f \in ⋃ ran Fil ⟼ \{x \in ⋃ j \| (nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j)\})$
22	0 21	wceq	$wff fLim = (j \in Top, f \in ⋃ ran Fil ⟼ \{x \in ⋃ j \| (nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j)\})$

Metamath Proof Explorer