Metamath Proof Explorer

Theorem cfilucfil3

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion cfilucfil3 ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ Fil ⁡ X ∧ C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ CauFil ⁡ D

Proof

Step Hyp Ref Expression
1 xmetpsmet ⊢ D ∈ ∞Met ⁡ X → D ∈ PsMet ⁡ X
2 cfilucfil2 ⊢ X ≠ ∅ ∧ D ∈ PsMet ⁡ X → C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ fBas ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
3 2 anbi2d ⊢ X ≠ ∅ ∧ D ∈ PsMet ⁡ X → C ∈ Fil ⁡ X ∧ C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ Fil ⁡ X ∧ C ∈ fBas ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
4 filfbas ⊢ C ∈ Fil ⁡ X → C ∈ fBas ⁡ X
5 4 pm4.71i ⊢ C ∈ Fil ⁡ X ↔ C ∈ Fil ⁡ X ∧ C ∈ fBas ⁡ X
6 5 anbi1i ⊢ C ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x ↔ C ∈ Fil ⁡ X ∧ C ∈ fBas ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
7 anass ⊢ C ∈ Fil ⁡ X ∧ C ∈ fBas ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x ↔ C ∈ Fil ⁡ X ∧ C ∈ fBas ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
8 6 7 bitr2i ⊢ C ∈ Fil ⁡ X ∧ C ∈ fBas ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x ↔ C ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
9 3 8 bitrdi ⊢ X ≠ ∅ ∧ D ∈ PsMet ⁡ X → C ∈ Fil ⁡ X ∧ C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
10 1 9 sylan2 ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ Fil ⁡ X ∧ C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
11 iscfil ⊢ D ∈ ∞Met ⁡ X → C ∈ CauFil ⁡ D ↔ C ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
12 11 adantl ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ CauFil ⁡ D ↔ C ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ C D y × y ⊆ 0 x
13 10 12 bitr4d ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ Fil ⁡ X ∧ C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ CauFil ⁡ D