Definition 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 e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cflim	|- fLim
1		vj	|- j
2		ctop	|- Top
3		vf	|- f
4		cfil	|- Fil
5	4	crn	|- ran Fil
6	5	cuni	|- U. ran Fil
7		vx	|- x
8	1	cv	|- j
9	8	cuni	|- U. j
10		cnei	|- nei
11	8 10	cfv	|- ( nei ` j )
12	7	cv	|- x
13	12	csn	|- { x }
14	13 11	cfv	|- ( ( nei ` j ) ` { x } )
15	3	cv	|- f
16	14 15	wss	|- ( ( nei ` j ) ` { x } ) C_ f
17	9	cpw	|- ~P U. j
18	15 17	wss	|- f C_ ~P U. j
19	16 18	wa	|- ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j )
20	19 7 9	crab	|- { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) }
21	1 3 2 6 20	cmpo	|- ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } )
22	0 21	wceq	|- fLim = ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } )