Metamath Proof Explorer

Theorem cfilucfil4

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 cfilucfil4 ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X ∧ C ∈ Fil ⁡ X → C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ CauFil ⁡ D

Proof

Step Hyp Ref Expression
1 cfilucfil3 ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ Fil ⁡ X ∧ C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ CauFil ⁡ D
2 cfilfil ⊢ D ∈ ∞Met ⁡ X ∧ C ∈ CauFil ⁡ D → C ∈ Fil ⁡ X
3 2 ex ⊢ D ∈ ∞Met ⁡ X → C ∈ CauFil ⁡ D → C ∈ Fil ⁡ X
4 3 adantl ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ CauFil ⁡ D → C ∈ Fil ⁡ X
5 4 pm4.71rd ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ CauFil ⁡ D ↔ C ∈ Fil ⁡ X ∧ C ∈ CauFil ⁡ D
6 1 5 bitrd ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ Fil ⁡ X ∧ C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ Fil ⁡ X ∧ C ∈ CauFil ⁡ D
7 pm5.32 ⊢ C ∈ Fil ⁡ X → C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ CauFil ⁡ D ↔ C ∈ Fil ⁡ X ∧ C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ Fil ⁡ X ∧ C ∈ CauFil ⁡ D
8 6 7 sylibr ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X → C ∈ Fil ⁡ X → C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ CauFil ⁡ D
9 8 3impia ⊢ X ≠ ∅ ∧ D ∈ ∞Met ⁡ X ∧ C ∈ Fil ⁡ X → C ∈ CauFilU ⁡ metUnif ⁡ D ↔ C ∈ CauFil ⁡ D