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 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fClusf L ⁡ F ∧ N ∈ nei ⁡ J ⁡ A ∧ S ∈ L → N ∩ F S ≠ ∅

Proof

Step Hyp Ref Expression
1 fcfnei ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fClusf L ⁡ F ↔ A ∈ X ∧ ∀ n ∈ nei ⁡ J ⁡ A ∀ s ∈ L n ∩ F s ≠ ∅
2 ineq1 ⊢ n = N → n ∩ F s = N ∩ F s
3 2 neeq1d ⊢ n = N → n ∩ F s ≠ ∅ ↔ N ∩ F s ≠ ∅
4 imaeq2 ⊢ s = S → F s = F S
5 4 ineq2d ⊢ s = S → N ∩ F s = N ∩ F S
6 5 neeq1d ⊢ s = S → N ∩ F s ≠ ∅ ↔ N ∩ F S ≠ ∅
7 3 6 rspc2v ⊢ N ∈ nei ⁡ J ⁡ A ∧ S ∈ L → ∀ n ∈ nei ⁡ J ⁡ A ∀ s ∈ L n ∩ F s ≠ ∅ → N ∩ F S ≠ ∅
8 7 ex ⊢ N ∈ nei ⁡ J ⁡ A → S ∈ L → ∀ n ∈ nei ⁡ J ⁡ A ∀ s ∈ L n ∩ F s ≠ ∅ → N ∩ F S ≠ ∅
9 8 com3r ⊢ ∀ n ∈ nei ⁡ J ⁡ A ∀ s ∈ L n ∩ F s ≠ ∅ → N ∈ nei ⁡ J ⁡ A → S ∈ L → N ∩ F S ≠ ∅
10 9 adantl ⊢ A ∈ X ∧ ∀ n ∈ nei ⁡ J ⁡ A ∀ s ∈ L n ∩ F s ≠ ∅ → N ∈ nei ⁡ J ⁡ A → S ∈ L → N ∩ F S ≠ ∅
11 1 10 biimtrdi ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fClusf L ⁡ F → N ∈ nei ⁡ J ⁡ A → S ∈ L → N ∩ F S ≠ ∅
12 11 3imp2 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fClusf L ⁡ F ∧ N ∈ nei ⁡ J ⁡ A ∧ S ∈ L → N ∩ F S ≠ ∅