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 )