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

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 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐿 ) ) → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 fcfnei ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
2 ineq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) = ( 𝑁 ∩ ( 𝐹 “ 𝑠 ) ) )
3 2 neeq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ↔ ( 𝑁 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
4 imaeq2 ⊢ ( 𝑠 = 𝑆 → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ 𝑆 ) )
5 4 ineq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑁 ∩ ( 𝐹 “ 𝑠 ) ) = ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) )
6 5 neeq1d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑁 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ↔ ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) )
7 3 6 rspc2v ⊢ ( ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐿 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) )
8 7 ex ⊢ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑆 ∈ 𝐿 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) ) )
9 8 com3r ⊢ ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑆 ∈ 𝐿 → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) ) )
10 9 adantl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑆 ∈ 𝐿 → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) ) )
11 1 10 biimtrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑆 ∈ 𝐿 → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) ) ) )
12 11 3imp2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐿 ) ) → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ )