This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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