Definition df-flim 21743

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.)

Assertion

Ref	Expression
df-flim	|- fLim = ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } )

Distinct variable group:   f, j, x

Detailed syntax breakdown of Definition df-flim

Step	Hyp	Ref	Expression
1		cflim 21738	. 2 class fLim
2		vj	. . 3 setvar j
3		vf	. . 3 setvar f
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 U. ran Fil
8		vx	. . . . . . . . 9 setvar x
9	8	cv 1482	. . . . . . . 8 class x
10	9	csn 4177	. . . . . . 7 class { x }
11	2	cv 1482	. . . . . . . 8 class j
12		cnei 20901	. . . . . . . 8 class nei
13	11, 12	cfv 5888	. . . . . . 7 class ( nei ` j )
14	10, 13	cfv 5888	. . . . . 6 class ( ( nei ` j ) ` { x } )
15	3	cv 1482	. . . . . 6 class f
16	14, 15	wss 3574	. . . . 5 wff ( ( nei ` j ) ` { x } ) C_ f
17	11	cuni 4436	. . . . . . 7 class U. j
18	17	cpw 4158	. . . . . 6 class ~P U. j
19	15, 18	wss 3574	. . . . 5 wff f C_ ~P U. j
20	16, 19	wa 384	. . . 4 wff ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j )
21	20, 8, 17	crab 2916	. . 3 class { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) }
22	2, 3, 4, 7, 21	cmpt2 6652	. 2 class ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } )
23	1, 22	wceq 1483	1 wff fLim = ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } )

This definition is referenced by:  flimval  21767  elflim2  21768