Metamath Proof Explorer

Theorem equivtotbnd

Description: If the metric M is "strongly finer" than N (meaning that there is a positive real constant R such that N ( x , y ) <_ R x. M ( x , y ) ), then total boundedness of M implies total boundedness of N . (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses equivtotbnd.1 ⊢ ( 𝜑 → 𝑀 ∈ ( TotBnd ‘ 𝑋 ) )
equivtotbnd.2 ⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑋 ) )
equivtotbnd.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
equivtotbnd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
Assertion equivtotbnd ( 𝜑 → 𝑁 ∈ ( TotBnd ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 equivtotbnd.1 ⊢ ( 𝜑 → 𝑀 ∈ ( TotBnd ‘ 𝑋 ) )
2 equivtotbnd.2 ⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑋 ) )
3 equivtotbnd.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
4 equivtotbnd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑅 ∈ ℝ+ )
7 5 6 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 𝑅 ) ∈ ℝ+ )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑀 ∈ ( TotBnd ‘ 𝑋 ) )
9 istotbnd3 ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 ) )
10 9 simprbi ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → ∀ 𝑠 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 )
11 8 10 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑠 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 )
12 oveq2 ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) )
13 12 iuneq2d ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) )
14 13 eqeq1d ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 ↔ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 ) )
15 14 rexbidv ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 ) )
16 15 rspcv ⊢ ( ( 𝑟 / 𝑅 ) ∈ ℝ+ → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 ) )
17 7 11 16 sylc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 )
18 elfpw ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( 𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin ) )
19 18 simplbi ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑣 ⊆ 𝑋 )
20 19 adantl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑣 ⊆ 𝑋 )
21 20 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ 𝑋 )
22 eqid ⊢ ( MetOpen ‘ 𝑁 ) = ( MetOpen ‘ 𝑁 )
23 eqid ⊢ ( MetOpen ‘ 𝑀 ) = ( MetOpen ‘ 𝑀 )
24 9 simplbi ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
25 1 24 syl ⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
26 22 23 2 25 3 4 metss2lem ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
27 26 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
28 27 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
29 21 28 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
30 29 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
31 ss2iun ⊢ ( ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
32 30 31 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
33 sseq1 ⊢ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ↔ 𝑋 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ) )
34 32 33 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → 𝑋 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ) )
35 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑁 ∈ ( Met ‘ 𝑋 ) )
36 metxmet ⊢ ( 𝑁 ∈ ( Met ‘ 𝑋 ) → 𝑁 ∈ ( ∞Met ‘ 𝑋 ) )
37 35 36 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑁 ∈ ( ∞Met ‘ 𝑋 ) )
38 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑟 ∈ ℝ+ )
39 38 rpxrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑟 ∈ ℝ* )
40 blssm ⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
41 37 21 39 40 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
42 41 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
43 iunss ⊢ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 ↔ ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
44 42 43 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
45 34 44 jctild ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ) ) )
46 eqss ⊢ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 ↔ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ) )
47 45 46 syl6ibr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 ) )
48 47 reximdva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 ) )
49 17 48 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 )
50 49 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 )
51 istotbnd3 ⊢ ( 𝑁 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑁 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 ) )
52 2 50 51 sylanbrc ⊢ ( 𝜑 → 𝑁 ∈ ( TotBnd ‘ 𝑋 ) )