Metamath Proof Explorer

Theorem flimval

Description: The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flimval.1 
|- X = U. J
Assertion flimval 
|- ( ( J e. Top /\ F e. U. ran Fil ) -> ( J fLim F ) = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } )

Proof

Step Hyp Ref Expression
1 flimval.1 
 |-  X = U. J
2 1 topopn 
 |-  ( J e. Top -> X e. J )
3 2 adantr 
 |-  ( ( J e. Top /\ F e. U. ran Fil ) -> X e. J )
4 rabexg 
 |-  ( X e. J -> { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } e. _V )
5 3 4 syl 
 |-  ( ( J e. Top /\ F e. U. ran Fil ) -> { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } e. _V )
6 simpl 
 |-  ( ( j = J /\ f = F ) -> j = J )
7 6 unieqd 
 |-  ( ( j = J /\ f = F ) -> U. j = U. J )
8 7 1 eqtr4di 
 |-  ( ( j = J /\ f = F ) -> U. j = X )
9 6 fveq2d 
 |-  ( ( j = J /\ f = F ) -> ( nei ` j ) = ( nei ` J ) )
10 9 fveq1d 
 |-  ( ( j = J /\ f = F ) -> ( ( nei ` j ) ` { x } ) = ( ( nei ` J ) ` { x } ) )
11 simpr 
 |-  ( ( j = J /\ f = F ) -> f = F )
12 10 11 sseq12d 
 |-  ( ( j = J /\ f = F ) -> ( ( ( nei ` j ) ` { x } ) C_ f <-> ( ( nei ` J ) ` { x } ) C_ F ) )
13 8 pweqd 
 |-  ( ( j = J /\ f = F ) -> ~P U. j = ~P X )
14 11 13 sseq12d 
 |-  ( ( j = J /\ f = F ) -> ( f C_ ~P U. j <-> F C_ ~P X ) )
15 12 14 anbi12d 
 |-  ( ( j = J /\ f = F ) -> ( ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) <-> ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) ) )
16 8 15 rabeqbidv 
 |-  ( ( j = J /\ f = F ) -> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } )
17 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 ) } )
18 16 17 ovmpoga 
 |-  ( ( J e. Top /\ F e. U. ran Fil /\ { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } e. _V ) -> ( J fLim F ) = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } )
19 5 18 mpd3an3 
 |-  ( ( J e. Top /\ F e. U. ran Fil ) -> ( J fLim F ) = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } )