This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℝ + x ball ⁡ D s ⊆ x ball ⁡ C r ∧ ∀ a ∈ ℝ + ∃ b ∈ ℝ + x ball ⁡ C b ⊆ x ball ⁡ D a

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 ∈ ℝ + x ball ⁡ D s ⊆ x ball ⁡ C r
4 2 1 metss ⊢ D ∈ ∞Met ⁡ X ∧ C ∈ ∞Met ⁡ X → K ⊆ J ↔ ∀ x ∈ X ∀ a ∈ ℝ + ∃ b ∈ ℝ + x ball ⁡ C b ⊆ x ball ⁡ D a
5 4 ancoms ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ X → K ⊆ J ↔ ∀ x ∈ X ∀ a ∈ ℝ + ∃ b ∈ ℝ + x ball ⁡ C b ⊆ x ball ⁡ D a
6 3 5 anbi12d ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ X → J ⊆ K ∧ K ⊆ J ↔ ∀ x ∈ X ∀ r ∈ ℝ + ∃ s ∈ ℝ + x ball ⁡ D s ⊆ x ball ⁡ C r ∧ ∀ x ∈ X ∀ a ∈ ℝ + ∃ b ∈ ℝ + x ball ⁡ C b ⊆ x ball ⁡ D a
7 eqss ⊢ J = K ↔ J ⊆ K ∧ K ⊆ J
8 r19.26 ⊢ ∀ x ∈ X ∀ r ∈ ℝ + ∃ s ∈ ℝ + x ball ⁡ D s ⊆ x ball ⁡ C r ∧ ∀ a ∈ ℝ + ∃ b ∈ ℝ + x ball ⁡ C b ⊆ x ball ⁡ D a ↔ ∀ x ∈ X ∀ r ∈ ℝ + ∃ s ∈ ℝ + x ball ⁡ D s ⊆ x ball ⁡ C r ∧ ∀ x ∈ X ∀ a ∈ ℝ + ∃ b ∈ ℝ + x ball ⁡ C b ⊆ x ball ⁡ D a
9 6 7 8 3bitr4g ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ X → J = K ↔ ∀ x ∈ X ∀ r ∈ ℝ + ∃ s ∈ ℝ + x ball ⁡ D s ⊆ x ball ⁡ C r ∧ ∀ a ∈ ℝ + ∃ b ∈ ℝ + x ball ⁡ C b ⊆ x ball ⁡ D a