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