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

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 )