Metamath Proof Explorer

Theorem flftg

Description: Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 flftg.l ⊢ J = topGen ⁡ B
2 isflf ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ u ∈ J A ∈ u → ∃ s ∈ L F s ⊆ u
3 1 raleqi ⊢ ∀ u ∈ J A ∈ u → ∃ s ∈ L F s ⊆ u ↔ ∀ u ∈ topGen ⁡ B A ∈ u → ∃ s ∈ L F s ⊆ u
4 simpl1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → J ∈ TopOn ⁡ X
5 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
6 4 5 syl ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → J ∈ Top
7 1 6 eqeltrrid ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → topGen ⁡ B ∈ Top
8 tgclb ⊢ B ∈ TopBases ↔ topGen ⁡ B ∈ Top
9 7 8 sylibr ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → B ∈ TopBases
10 bastg ⊢ B ∈ TopBases → B ⊆ topGen ⁡ B
11 eleq2w ⊢ u = o → A ∈ u ↔ A ∈ o
12 sseq2 ⊢ u = o → F s ⊆ u ↔ F s ⊆ o
13 12 rexbidv ⊢ u = o → ∃ s ∈ L F s ⊆ u ↔ ∃ s ∈ L F s ⊆ o
14 11 13 imbi12d ⊢ u = o → A ∈ u → ∃ s ∈ L F s ⊆ u ↔ A ∈ o → ∃ s ∈ L F s ⊆ o
15 14 cbvralvw ⊢ ∀ u ∈ topGen ⁡ B A ∈ u → ∃ s ∈ L F s ⊆ u ↔ ∀ o ∈ topGen ⁡ B A ∈ o → ∃ s ∈ L F s ⊆ o
16 ssralv ⊢ B ⊆ topGen ⁡ B → ∀ o ∈ topGen ⁡ B A ∈ o → ∃ s ∈ L F s ⊆ o → ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o
17 15 16 syl5bi ⊢ B ⊆ topGen ⁡ B → ∀ u ∈ topGen ⁡ B A ∈ u → ∃ s ∈ L F s ⊆ u → ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o
18 9 10 17 3syl ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → ∀ u ∈ topGen ⁡ B A ∈ u → ∃ s ∈ L F s ⊆ u → ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o
19 tg2 ⊢ u ∈ topGen ⁡ B ∧ A ∈ u → ∃ o ∈ B A ∈ o ∧ o ⊆ u
20 r19.29 ⊢ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o ∧ ∃ o ∈ B A ∈ o ∧ o ⊆ u → ∃ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o ∧ A ∈ o ∧ o ⊆ u
21 simpl ⊢ A ∈ o ∧ o ⊆ u → A ∈ o
22 simpr ⊢ A ∈ o ∧ o ⊆ u → o ⊆ u
23 sstr2 ⊢ F s ⊆ o → o ⊆ u → F s ⊆ u
24 22 23 syl5com ⊢ A ∈ o ∧ o ⊆ u → F s ⊆ o → F s ⊆ u
25 24 reximdv ⊢ A ∈ o ∧ o ⊆ u → ∃ s ∈ L F s ⊆ o → ∃ s ∈ L F s ⊆ u
26 21 25 embantd ⊢ A ∈ o ∧ o ⊆ u → A ∈ o → ∃ s ∈ L F s ⊆ o → ∃ s ∈ L F s ⊆ u
27 26 impcom ⊢ A ∈ o → ∃ s ∈ L F s ⊆ o ∧ A ∈ o ∧ o ⊆ u → ∃ s ∈ L F s ⊆ u
28 27 rexlimivw ⊢ ∃ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o ∧ A ∈ o ∧ o ⊆ u → ∃ s ∈ L F s ⊆ u
29 20 28 syl ⊢ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o ∧ ∃ o ∈ B A ∈ o ∧ o ⊆ u → ∃ s ∈ L F s ⊆ u
30 29 ex ⊢ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o → ∃ o ∈ B A ∈ o ∧ o ⊆ u → ∃ s ∈ L F s ⊆ u
31 19 30 syl5 ⊢ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o → u ∈ topGen ⁡ B ∧ A ∈ u → ∃ s ∈ L F s ⊆ u
32 31 expdimp ⊢ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o ∧ u ∈ topGen ⁡ B → A ∈ u → ∃ s ∈ L F s ⊆ u
33 32 ralrimiva ⊢ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o → ∀ u ∈ topGen ⁡ B A ∈ u → ∃ s ∈ L F s ⊆ u
34 18 33 impbid1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → ∀ u ∈ topGen ⁡ B A ∈ u → ∃ s ∈ L F s ⊆ u ↔ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o
35 3 34 syl5bb ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ X → ∀ u ∈ J A ∈ u → ∃ s ∈ L F s ⊆ u ↔ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o
36 35 pm5.32da ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ X ∧ ∀ u ∈ J A ∈ u → ∃ s ∈ L F s ⊆ u ↔ A ∈ X ∧ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o
37 2 36 bitrd ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fLimf L ⁡ F ↔ A ∈ X ∧ ∀ o ∈ B A ∈ o → ∃ s ∈ L F s ⊆ o