# 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 ${⊢}{\phi }\to {M}\in \mathrm{TotBnd}\left({X}\right)$
equivtotbnd.2 ${⊢}{\phi }\to {N}\in \mathrm{Met}\left({X}\right)$
equivtotbnd.3 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
equivtotbnd.4 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
Assertion equivtotbnd ${⊢}{\phi }\to {N}\in \mathrm{TotBnd}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 equivtotbnd.1 ${⊢}{\phi }\to {M}\in \mathrm{TotBnd}\left({X}\right)$
2 equivtotbnd.2 ${⊢}{\phi }\to {N}\in \mathrm{Met}\left({X}\right)$
3 equivtotbnd.3 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
4 equivtotbnd.4 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
5 simpr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to {r}\in {ℝ}^{+}$
6 3 adantr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to {R}\in {ℝ}^{+}$
7 5 6 rpdivcld ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \frac{{r}}{{R}}\in {ℝ}^{+}$
8 1 adantr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to {M}\in \mathrm{TotBnd}\left({X}\right)$
9 istotbnd3 ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){s}\right)={X}\right)$
10 9 simprbi ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to \forall {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){s}\right)={X}$
11 8 10 syl ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \forall {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){s}\right)={X}$
12 oveq2 ${⊢}{s}=\frac{{r}}{{R}}\to {x}\mathrm{ball}\left({M}\right){s}={x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)$
13 12 iuneq2d ${⊢}{s}=\frac{{r}}{{R}}\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){s}\right)=\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)$
14 13 eqeq1d ${⊢}{s}=\frac{{r}}{{R}}\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){s}\right)={X}↔\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}\right)$
15 14 rexbidv ${⊢}{s}=\frac{{r}}{{R}}\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){s}\right)={X}↔\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}\right)$
16 15 rspcv ${⊢}\frac{{r}}{{R}}\in {ℝ}^{+}\to \left(\forall {s}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){s}\right)={X}\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}\right)$
17 7 11 16 sylc ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}$
18 elfpw ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)↔\left({v}\subseteq {X}\wedge {v}\in \mathrm{Fin}\right)$
19 18 simplbi ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {v}\subseteq {X}$
20 19 adantl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to {v}\subseteq {X}$
21 20 sselda ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {x}\in {X}$
22 eqid ${⊢}\mathrm{MetOpen}\left({N}\right)=\mathrm{MetOpen}\left({N}\right)$
23 eqid ${⊢}\mathrm{MetOpen}\left({M}\right)=\mathrm{MetOpen}\left({M}\right)$
24 9 simplbi ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to {M}\in \mathrm{Met}\left({X}\right)$
25 1 24 syl ${⊢}{\phi }\to {M}\in \mathrm{Met}\left({X}\right)$
26 22 23 2 25 3 4 metss2lem ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {r}\in {ℝ}^{+}\right)\right)\to {x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\subseteq {x}\mathrm{ball}\left({N}\right){r}$
27 26 anass1rs ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\subseteq {x}\mathrm{ball}\left({N}\right){r}$
28 27 adantlr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {X}\right)\to {x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\subseteq {x}\mathrm{ball}\left({N}\right){r}$
29 21 28 syldan ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\subseteq {x}\mathrm{ball}\left({N}\right){r}$
30 29 ralrimiva ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\subseteq {x}\mathrm{ball}\left({N}\right){r}$
31 ss2iun ${⊢}\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\subseteq {x}\mathrm{ball}\left({N}\right){r}\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)$
32 30 31 syl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)$
33 sseq1 ${⊢}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)↔{X}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)\right)$
34 32 33 syl5ibcom ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}\to {X}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)\right)$
35 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {N}\in \mathrm{Met}\left({X}\right)$
36 metxmet ${⊢}{N}\in \mathrm{Met}\left({X}\right)\to {N}\in \mathrm{\infty Met}\left({X}\right)$
37 35 36 syl ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {N}\in \mathrm{\infty Met}\left({X}\right)$
38 simpllr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {r}\in {ℝ}^{+}$
39 38 rpxrd ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {r}\in {ℝ}^{*}$
40 blssm ${⊢}\left({N}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to {x}\mathrm{ball}\left({N}\right){r}\subseteq {X}$
41 37 21 39 40 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {x}\mathrm{ball}\left({N}\right){r}\subseteq {X}$
42 41 ralrimiva ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({N}\right){r}\subseteq {X}$
43 iunss ${⊢}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)\subseteq {X}↔\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({N}\right){r}\subseteq {X}$
44 42 43 sylibr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)\subseteq {X}$
45 34 44 jctild ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)\subseteq {X}\wedge {X}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)\right)\right)$
46 eqss ${⊢}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)={X}↔\left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)\subseteq {X}\wedge {X}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)\right)$
47 45 46 syl6ibr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)={X}\right)$
48 47 reximdva ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{r}}{{R}}\right)\right)={X}\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)={X}\right)$
49 17 48 mpd ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)={X}$
50 49 ralrimiva ${⊢}{\phi }\to \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)={X}$
51 istotbnd3 ${⊢}{N}\in \mathrm{TotBnd}\left({X}\right)↔\left({N}\in \mathrm{Met}\left({X}\right)\wedge \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){r}\right)={X}\right)$
52 2 50 51 sylanbrc ${⊢}{\phi }\to {N}\in \mathrm{TotBnd}\left({X}\right)$