Metamath Proof Explorer

Theorem flffbas

Description: Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis flffbas.l ⊢ L = Y filGen B
Assertion flffbas ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ s ∈ B F s ⊆ o

Proof

Step Hyp Ref Expression
1 flffbas.l ⊢ L = Y filGen B
2 fgcl ⊢ B ∈ fBas ⁡ Y → Y filGen B ∈ Fil ⁡ Y
3 1 2 eqeltrid ⊢ B ∈ fBas ⁡ Y → L ∈ Fil ⁡ Y
4 isflf ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ t ∈ L F t ⊆ o
5 3 4 syl3an2 ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ t ∈ L F t ⊆ o
6 1 eleq2i ⊢ t ∈ L ↔ t ∈ Y filGen B
7 elfg ⊢ B ∈ fBas ⁡ Y → t ∈ Y filGen B ↔ t ⊆ Y ∧ ∃ s ∈ B s ⊆ t
8 7 3ad2ant2 ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → t ∈ Y filGen B ↔ t ⊆ Y ∧ ∃ s ∈ B s ⊆ t
9 sstr2 ⊢ F s ⊆ F t → F t ⊆ o → F s ⊆ o
10 imass2 ⊢ s ⊆ t → F s ⊆ F t
11 9 10 syl11 ⊢ F t ⊆ o → s ⊆ t → F s ⊆ o
12 11 adantl ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ F t ⊆ o → s ⊆ t → F s ⊆ o
13 12 reximdv ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ F t ⊆ o → ∃ s ∈ B s ⊆ t → ∃ s ∈ B F s ⊆ o
14 13 ex ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → F t ⊆ o → ∃ s ∈ B s ⊆ t → ∃ s ∈ B F s ⊆ o
15 14 com23 ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → ∃ s ∈ B s ⊆ t → F t ⊆ o → ∃ s ∈ B F s ⊆ o
16 15 adantld ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → t ⊆ Y ∧ ∃ s ∈ B s ⊆ t → F t ⊆ o → ∃ s ∈ B F s ⊆ o
17 8 16 sylbid ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → t ∈ Y filGen B → F t ⊆ o → ∃ s ∈ B F s ⊆ o
18 17 adantr ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → t ∈ Y filGen B → F t ⊆ o → ∃ s ∈ B F s ⊆ o
19 6 18 biimtrid ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → t ∈ L → F t ⊆ o → ∃ s ∈ B F s ⊆ o
20 19 rexlimdv ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → ∃ t ∈ L F t ⊆ o → ∃ s ∈ B F s ⊆ o
21 ssfg ⊢ B ∈ fBas ⁡ Y → B ⊆ Y filGen B
22 21 1 sseqtrrdi ⊢ B ∈ fBas ⁡ Y → B ⊆ L
23 22 sselda ⊢ B ∈ fBas ⁡ Y ∧ s ∈ B → s ∈ L
24 23 3ad2antl2 ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ s ∈ B → s ∈ L
25 24 ad2ant2r ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X ∧ s ∈ B ∧ F s ⊆ o → s ∈ L
26 simprr ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X ∧ s ∈ B ∧ F s ⊆ o → F s ⊆ o
27 imaeq2 ⊢ t = s → F t = F s
28 27 sseq1d ⊢ t = s → F t ⊆ o ↔ F s ⊆ o
29 28 rspcev ⊢ s ∈ L ∧ F s ⊆ o → ∃ t ∈ L F t ⊆ o
30 25 26 29 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X ∧ s ∈ B ∧ F s ⊆ o → ∃ t ∈ L F t ⊆ o
31 30 rexlimdvaa ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → ∃ s ∈ B F s ⊆ o → ∃ t ∈ L F t ⊆ o
32 20 31 impbid ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → ∃ t ∈ L F t ⊆ o ↔ ∃ s ∈ B F s ⊆ o
33 32 imbi2d ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → A ∈ o → ∃ t ∈ L F t ⊆ o ↔ A ∈ o → ∃ s ∈ B F s ⊆ o
34 33 ralbidv ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → ∀ o ∈ J A ∈ o → ∃ t ∈ L F t ⊆ o ↔ ∀ o ∈ J A ∈ o → ∃ s ∈ B F s ⊆ o
35 34 pm5.32da ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ t ∈ L F t ⊆ o ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ s ∈ B F s ⊆ o
36 5 35 bitrd ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∃ s ∈ B F s ⊆ o