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

Metamath Proof Explorer

Theorem flimfil

Description: Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flimuni.1 
|- X = U. J
Assertion flimfil 
|- ( A e. ( J fLim F ) -> F e. ( Fil ` X ) )

Proof

Step Hyp Ref Expression
1 flimuni.1 
 |-  X = U. J
2 1 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 ) ) )
3 2 simplbi 
 |-  ( A e. ( J fLim F ) -> ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) )
4 3 simp2d 
 |-  ( A e. ( J fLim F ) -> F e. U. ran Fil )
5 filunirn 
 |-  ( F e. U. ran Fil <-> F e. ( Fil ` U. F ) )
6 4 5 sylib 
 |-  ( A e. ( J fLim F ) -> F e. ( Fil ` U. F ) )
7 3 simp3d 
 |-  ( A e. ( J fLim F ) -> F C_ ~P X )
8 sspwuni 
 |-  ( F C_ ~P X <-> U. F C_ X )
9 7 8 sylib 
 |-  ( A e. ( J fLim F ) -> U. F C_ X )
10 flimneiss 
 |-  ( A e. ( J fLim F ) -> ( ( nei ` J ) ` { A } ) C_ F )
11 flimtop 
 |-  ( A e. ( J fLim F ) -> J e. Top )
12 1 topopn 
 |-  ( J e. Top -> X e. J )
13 11 12 syl 
 |-  ( A e. ( J fLim F ) -> X e. J )
14 1 flimelbas 
 |-  ( A e. ( J fLim F ) -> A e. X )
15 opnneip 
 |-  ( ( J e. Top /\ X e. J /\ A e. X ) -> X e. ( ( nei ` J ) ` { A } ) )
16 11 13 14 15 syl3anc 
 |-  ( A e. ( J fLim F ) -> X e. ( ( nei ` J ) ` { A } ) )
17 10 16 sseldd 
 |-  ( A e. ( J fLim F ) -> X e. F )
18 elssuni 
 |-  ( X e. F -> X C_ U. F )
19 17 18 syl 
 |-  ( A e. ( J fLim F ) -> X C_ U. F )
20 9 19 eqssd 
 |-  ( A e. ( J fLim F ) -> U. F = X )
21 20 fveq2d 
 |-  ( A e. ( J fLim F ) -> ( Fil ` U. F ) = ( Fil ` X ) )
22 6 21 eleqtrd 
 |-  ( A e. ( J fLim F ) -> F e. ( Fil ` X ) )