Metamath Proof Explorer

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 syl6ib ⊢ ( ( ( 𝐶 ∈ ( ∞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 ‘ 𝐷 ) 𝑠 ) ) → 𝐽 = 𝐾 ) )