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∈CDy×y⊆0x
3 2 anbi2d ⊢X≠∅∧D∈PsMet⁡X→C∈Fil⁡X∧C∈CauFilU⁡metUnif⁡D↔C∈Fil⁡X∧C∈fBas⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x
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∈CDy×y⊆0x↔C∈Fil⁡X∧C∈fBas⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x
7 anass ⊢C∈Fil⁡X∧C∈fBas⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x↔C∈Fil⁡X∧C∈fBas⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x
8 6 7 bitr2i ⊢C∈Fil⁡X∧C∈fBas⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x↔C∈Fil⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x
9 3 8 bitrdi ⊢X≠∅∧D∈PsMet⁡X→C∈Fil⁡X∧C∈CauFilU⁡metUnif⁡D↔C∈Fil⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x
10 1 9 sylan2 ⊢X≠∅∧D∈∞Met⁡X→C∈Fil⁡X∧C∈CauFilU⁡metUnif⁡D↔C∈Fil⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x
11 iscfil ⊢D∈∞Met⁡X→C∈CauFil⁡D↔C∈Fil⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x
12 11 adantl ⊢X≠∅∧D∈∞Met⁡X→C∈CauFil⁡D↔C∈Fil⁡X∧∀x∈ℝ+∃y∈CDy×y⊆0x
13 10 12 bitr4d ⊢X≠∅∧D∈∞Met⁡X→C∈Fil⁡X∧C∈CauFilU⁡metUnif⁡D↔C∈CauFil⁡D