Metamath Proof Explorer

Theorem fcfneii

Description: A neighborhood of a cluster point of a function contains a function value from every tail. (Contributed by Jeff Hankins, 27-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion fcfneii 
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fClusf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. L ) ) -> ( N i^i ( F " S ) ) =/= (/) )

Proof

Step Hyp Ref Expression
1 fcfnei 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) ) ) )
2 ineq1 
 |-  ( n = N -> ( n i^i ( F " s ) ) = ( N i^i ( F " s ) ) )
3 2 neeq1d 
 |-  ( n = N -> ( ( n i^i ( F " s ) ) =/= (/) <-> ( N i^i ( F " s ) ) =/= (/) ) )
4 imaeq2 
 |-  ( s = S -> ( F " s ) = ( F " S ) )
5 4 ineq2d 
 |-  ( s = S -> ( N i^i ( F " s ) ) = ( N i^i ( F " S ) ) )
6 5 neeq1d 
 |-  ( s = S -> ( ( N i^i ( F " s ) ) =/= (/) <-> ( N i^i ( F " S ) ) =/= (/) ) )
7 3 6 rspc2v 
 |-  ( ( N e. ( ( nei ` J ) ` { A } ) /\ S e. L ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) -> ( N i^i ( F " S ) ) =/= (/) ) )
8 7 ex 
 |-  ( N e. ( ( nei ` J ) ` { A } ) -> ( S e. L -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) -> ( N i^i ( F " S ) ) =/= (/) ) ) )
9 8 com3r 
 |-  ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) -> ( N e. ( ( nei ` J ) ` { A } ) -> ( S e. L -> ( N i^i ( F " S ) ) =/= (/) ) ) )
10 9 adantl 
 |-  ( ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) ) -> ( N e. ( ( nei ` J ) ` { A } ) -> ( S e. L -> ( N i^i ( F " S ) ) =/= (/) ) ) )
11 1 10 syl6bi 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) -> ( N e. ( ( nei ` J ) ` { A } ) -> ( S e. L -> ( N i^i ( F " S ) ) =/= (/) ) ) ) )
12 11 3imp2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fClusf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. L ) ) -> ( N i^i ( F " S ) ) =/= (/) )