Metamath Proof Explorer

Theorem isflf

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

Ref Expression
Assertion isflf ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ s ∈ L F s ⊆ o

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 flimopn ⊢ J ∈ TopOn ⁡ X ∧ X FilMap F ⁡ L ∈ Fil ⁡ X → A ∈ J fLim X FilMap F ⁡ L ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → o ∈ 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 ∧ ∀ o ∈ J A ∈ o → o ∈ X FilMap F ⁡ L
13 toponss ⊢ J ∈ TopOn ⁡ X ∧ o ∈ J → o ⊆ X
14 3 13 sylan ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ o ∈ J → o ⊆ X
15 elfm ⊢ X ∈ J ∧ L ∈ fBas ⁡ Y ∧ F : Y ⟶ X → o ∈ X FilMap F ⁡ L ↔ o ⊆ X ∧ ∃ s ∈ L F s ⊆ o
16 5 7 8 15 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → o ∈ X FilMap F ⁡ L ↔ o ⊆ X ∧ ∃ s ∈ L F s ⊆ o
17 16 adantr ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ o ∈ J → o ∈ X FilMap F ⁡ L ↔ o ⊆ X ∧ ∃ s ∈ L F s ⊆ o
18 14 17 mpbirand ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ o ∈ J → o ∈ X FilMap F ⁡ L ↔ ∃ s ∈ L F s ⊆ o
19 18 imbi2d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ o ∈ J → A ∈ o → o ∈ X FilMap F ⁡ L ↔ A ∈ o → ∃ s ∈ L F s ⊆ o
20 19 ralbidva ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → ∀ o ∈ J A ∈ o → o ∈ X FilMap F ⁡ L ↔ ∀ o ∈ J A ∈ o → ∃ s ∈ L F s ⊆ o
21 20 anbi2d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ X ∧ ∀ o ∈ J A ∈ o → o ∈ X FilMap F ⁡ L ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ s ∈ L F s ⊆ o
22 2 12 21 3bitrd ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ s ∈ L F s ⊆ o