Metamath Proof Explorer

Theorem elflim2

Description: The predicate "is a limit point of a filter." (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 6-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 flimval.1 
 |-  X = U. J
2 anass 
 |-  ( ( ( ( J e. Top /\ F e. U. ran Fil ) /\ F C_ ~P X ) /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) <-> ( ( J e. Top /\ F e. U. ran Fil ) /\ ( F C_ ~P X /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) ) )
3 df-3an 
 |-  ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) <-> ( ( J e. Top /\ F e. U. ran Fil ) /\ F C_ ~P X ) )
4 3 anbi1i 
 |-  ( ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) <-> ( ( ( J e. Top /\ F e. U. ran Fil ) /\ F C_ ~P X ) /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
5 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 ) } )
6 5 elmpocl 
 |-  ( A e. ( J fLim F ) -> ( J e. Top /\ F e. U. ran Fil ) )
7 1 flimval 
 |-  ( ( J e. Top /\ F e. U. ran Fil ) -> ( J fLim F ) = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } )
8 7 eleq2d 
 |-  ( ( J e. Top /\ F e. U. ran Fil ) -> ( A e. ( J fLim F ) <-> A e. { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } ) )
9 sneq 
 |-  ( x = A -> { x } = { A } )
10 9 fveq2d 
 |-  ( x = A -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { A } ) )
11 10 sseq1d 
 |-  ( x = A -> ( ( ( nei ` J ) ` { x } ) C_ F <-> ( ( nei ` J ) ` { A } ) C_ F ) )
12 11 anbi1d 
 |-  ( x = A -> ( ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) <-> ( ( ( nei ` J ) ` { A } ) C_ F /\ F C_ ~P X ) ) )
13 12 biancomd 
 |-  ( x = A -> ( ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) <-> ( F C_ ~P X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
14 13 elrab 
 |-  ( A e. { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } <-> ( A e. X /\ ( F C_ ~P X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
15 an12 
 |-  ( ( A e. X /\ ( F C_ ~P X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) <-> ( F C_ ~P X /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
16 14 15 bitri 
 |-  ( A e. { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } <-> ( F C_ ~P X /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
17 8 16 bitrdi 
 |-  ( ( J e. Top /\ F e. U. ran Fil ) -> ( A e. ( J fLim F ) <-> ( F C_ ~P X /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) ) )
18 6 17 biadanii 
 |-  ( A e. ( J fLim F ) <-> ( ( J e. Top /\ F e. U. ran Fil ) /\ ( F C_ ~P X /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) ) )
19 2 4 18 3bitr4ri 
 |-  ( A e. ( J fLim F ) <-> ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )