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 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metequiv.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion metequiv ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐽 = 𝐾 ↔ ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑎 ) ) ) )

Proof

Step Hyp Ref Expression
1 metequiv.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metequiv.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 1 2 metss ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
4 2 1 metss ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐾 ⊆ 𝐽 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑎 ) ) )
5 4 ancoms ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐾 ⊆ 𝐽 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑎 ) ) )
6 3 5 anbi12d ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ( 𝐽 ⊆ 𝐾 ∧ 𝐾 ⊆ 𝐽 ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑎 ) ) ) )
7 eqss ⊢ ( 𝐽 = 𝐾 ↔ ( 𝐽 ⊆ 𝐾 ∧ 𝐾 ⊆ 𝐽 ) )
8 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑎 ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑎 ) ) )
9 6 7 8 3bitr4g ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐽 = 𝐾 ↔ ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑏 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑎 ) ) ) )