Metamath Proof Explorer

Theorem flfnei

Description: The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion 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

Proof

Step Hyp Ref Expression
1 flfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
2 1 eleq2d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ J fLim X FilMap F ⁡ L
3 simp1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J ∈ TopOn ⁡ X
4 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
5 4 3ad2ant1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → X ∈ J
6 filfbas ⊢ L ∈ Fil ⁡ Y → L ∈ fBas ⁡ Y
7 6 3ad2ant2 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → L ∈ fBas ⁡ Y
8 simp3 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → F : Y ⟶ X
9 fmfil ⊢ X ∈ J ∧ L ∈ fBas ⁡ Y ∧ F : Y ⟶ X → X FilMap F ⁡ L ∈ Fil ⁡ X
10 5 7 8 9 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → X FilMap F ⁡ L ∈ Fil ⁡ X
11 elflim ⊢ J ∈ TopOn ⁡ X ∧ X FilMap F ⁡ L ∈ Fil ⁡ X → A ∈ J fLim X FilMap F ⁡ L ↔ A ∈ X ∧ nei ⁡ J ⁡ A ⊆ X FilMap F ⁡ L
12 3 10 11 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLim X FilMap F ⁡ L ↔ A ∈ X ∧ nei ⁡ J ⁡ A ⊆ X FilMap F ⁡ L
13 dfss3 ⊢ nei ⁡ J ⁡ A ⊆ X FilMap F ⁡ L ↔ ∀ n ∈ nei ⁡ J ⁡ A n ∈ X FilMap F ⁡ L
14 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
15 14 3ad2ant1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J ∈ Top
16 eqid ⊢ ⋃ J = ⋃ J
17 16 neii1 ⊢ J ∈ Top ∧ n ∈ nei ⁡ J ⁡ A → n ⊆ ⋃ J
18 15 17 sylan ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ n ∈ nei ⁡ J ⁡ A → n ⊆ ⋃ J
19 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
20 19 3ad2ant1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → X = ⋃ J
21 20 adantr ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ n ∈ nei ⁡ J ⁡ A → X = ⋃ J
22 18 21 sseqtrrd ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ n ∈ nei ⁡ J ⁡ A → n ⊆ X
23 elfm ⊢ X ∈ J ∧ L ∈ fBas ⁡ Y ∧ F : Y ⟶ X → n ∈ X FilMap F ⁡ L ↔ n ⊆ X ∧ ∃ s ∈ L F s ⊆ n
24 5 7 8 23 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → n ∈ X FilMap F ⁡ L ↔ n ⊆ X ∧ ∃ s ∈ L F s ⊆ n
25 24 baibd ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ n ⊆ X → n ∈ X FilMap F ⁡ L ↔ ∃ s ∈ L F s ⊆ n
26 22 25 syldan ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ n ∈ nei ⁡ J ⁡ A → n ∈ X FilMap F ⁡ L ↔ ∃ s ∈ L F s ⊆ n
27 26 ralbidva ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → ∀ n ∈ nei ⁡ J ⁡ A n ∈ X FilMap F ⁡ L ↔ ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n
28 13 27 bitrid ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → nei ⁡ J ⁡ A ⊆ X FilMap F ⁡ L ↔ ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n
29 28 anbi2d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ X ∧ nei ⁡ J ⁡ A ⊆ X FilMap F ⁡ L ↔ A ∈ X ∧ ∀ n ∈ nei ⁡ J ⁡ A ∃ s ∈ L F s ⊆ n
30 2 12 29 3bitrd ⊢ 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