Metamath Proof Explorer


Theorem flfneii

Description: A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flfneii.x
|- X = U. J
Assertion flfneii
|- ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> E. s e. L ( F " s ) C_ N )

Proof

Step Hyp Ref Expression
1 flfneii.x
 |-  X = U. J
2 1 toptopon
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
3 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 ) ) )
4 2 3 syl3an1b
 |-  ( ( J e. Top /\ 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 ) ) )
5 4 simplbda
 |-  ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) ) -> A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n )
6 5 3adant3
 |-  ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n )
7 sseq2
 |-  ( n = N -> ( ( F " s ) C_ n <-> ( F " s ) C_ N ) )
8 7 rexbidv
 |-  ( n = N -> ( E. s e. L ( F " s ) C_ n <-> E. s e. L ( F " s ) C_ N ) )
9 8 rspcv
 |-  ( N e. ( ( nei ` J ) ` { A } ) -> ( A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n -> E. s e. L ( F " s ) C_ N ) )
10 9 3ad2ant3
 |-  ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> ( A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n -> E. s e. L ( F " s ) C_ N ) )
11 6 10 mpd
 |-  ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> E. s e. L ( F " s ) C_ N )