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 = ⋃ J
Assertion flfneii ⊢ J ∈ Top ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ N ∈ nei ⁡ J ⁡ A → ∃ s ∈ L F s ⊆ N

Proof

Step Hyp Ref Expression
1 flfneii.x ⊢ X = ⋃ J
2 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
3 flfnei ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n
4 2 3 syl3an1b ⊢ J ∈ Top ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n
5 4 simplbda ⊢ J ∈ Top ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F → ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n
6 5 3adant3 ⊢ J ∈ Top ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ N ∈ nei ⁡ J ⁡ A → ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n
7 sseq2 ⊢ n = N → F s ⊆ n ↔ F s ⊆ N
8 7 rexbidv ⊢ n = N → ∃ s ∈ L F s ⊆ n ↔ ∃ s ∈ L F s ⊆ N
9 8 rspcv ⊢ N ∈ nei ⁡ J ⁡ A → ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n → ∃ s ∈ L F s ⊆ N
10 9 3ad2ant3 ⊢ J ∈ Top ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ N ∈ nei ⁡ J ⁡ A → ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n → ∃ s ∈ L F s ⊆ N
11 6 10 mpd ⊢ J ∈ Top ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fLimf L ⁡ F ∧ N ∈ nei ⁡ J ⁡ A → ∃ s ∈ L F s ⊆ N