Metamath Proof Explorer


Theorem flfnei

Description: The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flfnei
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) )

Proof

Step Hyp Ref Expression
1 flfval
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
2 1 eleq2d
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> A e. ( J fLim ( ( X FilMap F ) ` L ) ) ) )
3 simp1
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> J e. ( TopOn ` X ) )
4 toponmax
 |-  ( J e. ( TopOn ` X ) -> X e. J )
5 4 3ad2ant1
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> X e. J )
6 filfbas
 |-  ( L e. ( Fil ` Y ) -> L e. ( fBas ` Y ) )
7 6 3ad2ant2
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> L e. ( fBas ` Y ) )
8 simp3
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> F : Y --> X )
9 fmfil
 |-  ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) )
10 5 7 8 9 syl3anc
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) )
11 elflim
 |-  ( ( J e. ( TopOn ` X ) /\ ( ( X FilMap F ) ` L ) e. ( Fil ` X ) ) -> ( A e. ( J fLim ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) ) ) )
12 3 10 11 syl2anc
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( J fLim ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) ) ) )
13 dfss3
 |-  ( ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) <-> A. n e. ( ( nei ` J ) ` { A } ) n e. ( ( X FilMap F ) ` L ) )
14 topontop
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
15 14 3ad2ant1
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> J e. Top )
16 eqid
 |-  U. J = U. J
17 16 neii1
 |-  ( ( J e. Top /\ n e. ( ( nei ` J ) ` { A } ) ) -> n C_ U. J )
18 15 17 sylan
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> n C_ U. J )
19 toponuni
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
20 19 3ad2ant1
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> X = U. J )
21 20 adantr
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> X = U. J )
22 18 21 sseqtrrd
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> n C_ X )
23 elfm
 |-  ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( n e. ( ( X FilMap F ) ` L ) <-> ( n C_ X /\ E. s e. L ( F " s ) C_ n ) ) )
24 5 7 8 23 syl3anc
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( n e. ( ( X FilMap F ) ` L ) <-> ( n C_ X /\ E. s e. L ( F " s ) C_ n ) ) )
25 24 baibd
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n C_ X ) -> ( n e. ( ( X FilMap F ) ` L ) <-> E. s e. L ( F " s ) C_ n ) )
26 22 25 syldan
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( n e. ( ( X FilMap F ) ` L ) <-> E. s e. L ( F " s ) C_ n ) )
27 26 ralbidva
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A. n e. ( ( nei ` J ) ` { A } ) n e. ( ( X FilMap F ) ` L ) <-> A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) )
28 13 27 syl5bb
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) <-> A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) )
29 28 anbi2d
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) )
30 2 12 29 3bitrd
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) )