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 ‘ 𝐷 ) 𝑎 ) ) ) )