Metamath Proof Explorer

Theorem fbflim

Description: A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis fbflim.3 ⊢ F = X filGen B
Assertion fbflim ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X → A ∈ J fLim F ↔ A ∈ X ∧ ∀ x ∈ J A ∈ x → ∃ y ∈ B y ⊆ x

Proof

Step Hyp Ref Expression
1 fbflim.3 ⊢ F = X filGen B
2 fgcl ⊢ B ∈ fBas ⁡ X → X filGen B ∈ Fil ⁡ X
3 1 2 eqeltrid ⊢ B ∈ fBas ⁡ X → F ∈ Fil ⁡ X
4 flimopn ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fLim F ↔ A ∈ X ∧ ∀ x ∈ J A ∈ x → x ∈ F
5 3 4 sylan2 ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X → A ∈ J fLim F ↔ A ∈ X ∧ ∀ x ∈ J A ∈ x → x ∈ F
6 toponss ⊢ J ∈ TopOn ⁡ X ∧ x ∈ J → x ⊆ X
7 6 ad4ant14 ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X ∧ A ∈ X ∧ x ∈ J → x ⊆ X
8 1 eleq2i ⊢ x ∈ F ↔ x ∈ X filGen B
9 elfg ⊢ B ∈ fBas ⁡ X → x ∈ X filGen B ↔ x ⊆ X ∧ ∃ y ∈ B y ⊆ x
10 9 ad3antlr ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X ∧ A ∈ X ∧ x ∈ J → x ∈ X filGen B ↔ x ⊆ X ∧ ∃ y ∈ B y ⊆ x
11 8 10 syl5bb ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X ∧ A ∈ X ∧ x ∈ J → x ∈ F ↔ x ⊆ X ∧ ∃ y ∈ B y ⊆ x
12 7 11 mpbirand ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X ∧ A ∈ X ∧ x ∈ J → x ∈ F ↔ ∃ y ∈ B y ⊆ x
13 12 imbi2d ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X ∧ A ∈ X ∧ x ∈ J → A ∈ x → x ∈ F ↔ A ∈ x → ∃ y ∈ B y ⊆ x
14 13 ralbidva ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X ∧ A ∈ X → ∀ x ∈ J A ∈ x → x ∈ F ↔ ∀ x ∈ J A ∈ x → ∃ y ∈ B y ⊆ x
15 14 pm5.32da ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X → A ∈ X ∧ ∀ x ∈ J A ∈ x → x ∈ F ↔ A ∈ X ∧ ∀ x ∈ J A ∈ x → ∃ y ∈ B y ⊆ x
16 5 15 bitrd ⊢ J ∈ TopOn ⁡ X ∧ B ∈ fBas ⁡ X → A ∈ J fLim F ↔ A ∈ X ∧ ∀ x ∈ J A ∈ x → ∃ y ∈ B y ⊆ x