Theorem metequiv2

Description: If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Hypotheses	metequiv.3	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
	metequiv.4	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion	metequiv2	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → 𝐽 = 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		metequiv.3	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2		metequiv.4	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3		simprrr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) )
4		simplll	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
5		simplr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → 𝑥 ∈ 𝑋 )
6		simprlr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → 𝑠 ∈ ℝ+ )
7	6	rpxrd	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → 𝑠 ∈ ℝ* )
8		simprll	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → 𝑟 ∈ ℝ+ )
9	8	rpxrd	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → 𝑟 ∈ ℝ* )
10		simprrl	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → 𝑠 ≤ 𝑟 )
11		ssbl	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑠 ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) ∧ 𝑠 ≤ 𝑟 ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
12	4 5 7 9 10 11	syl221anc	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
13	3 12	eqsstrrd	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
14		simpllr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
15		ssbl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑠 ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) ∧ 𝑠 ≤ 𝑟 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
16	14 5 7 9 10 15	syl221anc	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
17	3 16	eqsstrd	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
18	13 17	jca	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) ) ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
19	18	expr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ( ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
20	19	anassrs	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑠 ∈ ℝ+ ) → ( ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
21	20	reximdva	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → ∃ 𝑠 ∈ ℝ+ ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
22		r19.40	⊢ ( ∃ 𝑠 ∈ ℝ+ ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
23	21 22	syl6	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
24	23	ralimdva	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → ∀ 𝑟 ∈ ℝ+ ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
25		r19.26	⊢ ( ∀ 𝑟 ∈ ℝ+ ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ↔ ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
26	24 25	imbitrdi	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
27	26	ralimdva	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
28	1 2	metequiv	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐽 = 𝐾 ↔ ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
29	27 28	sylibrd	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ) → 𝐽 = 𝐾 ) )