Metamath Proof Explorer

Theorem metequiv

Description: Two ways of saying that two metrics generate the same topology. Two metrics satisfying the right-hand side are said to be (topologically) equivalent. (Contributed by Jeff Hankins, 21-Jun-2009) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypotheses metequiv.3 ⊢J=MetOpen⁡C
metequiv.4 ⊢K=MetOpen⁡D
Assertion metequiv ⊢C∈∞Met⁡X∧D∈∞Met⁡X→J=K↔∀x∈X∀r∈ℝ+∃s∈ℝ+xball⁡Ds⊆xball⁡Cr∧∀a∈ℝ+∃b∈ℝ+xball⁡Cb⊆xball⁡Da

Proof

Step Hyp Ref Expression
1 metequiv.3 ⊢J=MetOpen⁡C
2 metequiv.4 ⊢K=MetOpen⁡D
3 1 2 metss ⊢C∈∞Met⁡X∧D∈∞Met⁡X→J⊆K↔∀x∈X∀r∈ℝ+∃s∈ℝ+xball⁡Ds⊆xball⁡Cr
4 2 1 metss ⊢D∈∞Met⁡X∧C∈∞Met⁡X→K⊆J↔∀x∈X∀a∈ℝ+∃b∈ℝ+xball⁡Cb⊆xball⁡Da
5 4 ancoms ⊢C∈∞Met⁡X∧D∈∞Met⁡X→K⊆J↔∀x∈X∀a∈ℝ+∃b∈ℝ+xball⁡Cb⊆xball⁡Da
6 3 5 anbi12d ⊢C∈∞Met⁡X∧D∈∞Met⁡X→J⊆K∧K⊆J↔∀x∈X∀r∈ℝ+∃s∈ℝ+xball⁡Ds⊆xball⁡Cr∧∀x∈X∀a∈ℝ+∃b∈ℝ+xball⁡Cb⊆xball⁡Da
7 eqss ⊢J=K↔J⊆K∧K⊆J
8 r19.26 ⊢∀x∈X∀r∈ℝ+∃s∈ℝ+xball⁡Ds⊆xball⁡Cr∧∀a∈ℝ+∃b∈ℝ+xball⁡Cb⊆xball⁡Da↔∀x∈X∀r∈ℝ+∃s∈ℝ+xball⁡Ds⊆xball⁡Cr∧∀x∈X∀a∈ℝ+∃b∈ℝ+xball⁡Cb⊆xball⁡Da
9 6 7 8 3bitr4g ⊢C∈∞Met⁡X∧D∈∞Met⁡X→J=K↔∀x∈X∀r∈ℝ+∃s∈ℝ+xball⁡Ds⊆xball⁡Cr∧∀a∈ℝ+∃b∈ℝ+xball⁡Cb⊆xball⁡Da