Metamath Proof Explorer

Theorem elflim

Description: The predicate "is a limit point of a filter." (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion elflim 
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 1 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> J e. Top )
3 fvssunirn 
 |-  ( Fil ` X ) C_ U. ran Fil
4 3 sseli 
 |-  ( F e. ( Fil ` X ) -> F e. U. ran Fil )
5 4 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> F e. U. ran Fil )
6 filsspw 
 |-  ( F e. ( Fil ` X ) -> F C_ ~P X )
7 6 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> F C_ ~P X )
8 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
9 8 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> X = U. J )
10 9 pweqd 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ~P X = ~P U. J )
11 7 10 sseqtrd 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> F C_ ~P U. J )
12 eqid 
 |-  U. J = U. J
13 12 elflim2 
 |-  ( A e. ( J fLim F ) <-> ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P U. J ) /\ ( A e. U. J /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
14 13 baib 
 |-  ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P U. J ) -> ( A e. ( J fLim F ) <-> ( A e. U. J /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
15 2 5 11 14 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. U. J /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
16 9 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. X <-> A e. U. J ) )
17 16 anbi1d 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) <-> ( A e. U. J /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
18 15 17 bitr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )