Metamath Proof Explorer


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