Metamath Proof Explorer

Theorem equivbnd2

Description: If balls are totally bounded in the metric M , then balls are totally bounded in the equivalent metric N . (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Hypotheses equivbnd2.1 ${⊢}{\phi }\to {M}\in \mathrm{Met}\left({X}\right)$
equivbnd2.2 ${⊢}{\phi }\to {N}\in \mathrm{Met}\left({X}\right)$
equivbnd2.3 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
equivbnd2.4 ${⊢}{\phi }\to {S}\in {ℝ}^{+}$
equivbnd2.5 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
equivbnd2.6 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{M}{y}\le {S}\left({x}{N}{y}\right)$
equivbnd2.7 ${⊢}{C}={{M}↾}_{\left({Y}×{Y}\right)}$
equivbnd2.8 ${⊢}{D}={{N}↾}_{\left({Y}×{Y}\right)}$
equivbnd2.9 ${⊢}{\phi }\to \left({C}\in \mathrm{TotBnd}\left({Y}\right)↔{C}\in \mathrm{Bnd}\left({Y}\right)\right)$
Assertion equivbnd2 ${⊢}{\phi }\to \left({D}\in \mathrm{TotBnd}\left({Y}\right)↔{D}\in \mathrm{Bnd}\left({Y}\right)\right)$

Proof

Step Hyp Ref Expression
1 equivbnd2.1 ${⊢}{\phi }\to {M}\in \mathrm{Met}\left({X}\right)$
2 equivbnd2.2 ${⊢}{\phi }\to {N}\in \mathrm{Met}\left({X}\right)$
3 equivbnd2.3 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
4 equivbnd2.4 ${⊢}{\phi }\to {S}\in {ℝ}^{+}$
5 equivbnd2.5 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
6 equivbnd2.6 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{M}{y}\le {S}\left({x}{N}{y}\right)$
7 equivbnd2.7 ${⊢}{C}={{M}↾}_{\left({Y}×{Y}\right)}$
8 equivbnd2.8 ${⊢}{D}={{N}↾}_{\left({Y}×{Y}\right)}$
9 equivbnd2.9 ${⊢}{\phi }\to \left({C}\in \mathrm{TotBnd}\left({Y}\right)↔{C}\in \mathrm{Bnd}\left({Y}\right)\right)$
10 totbndbnd ${⊢}{D}\in \mathrm{TotBnd}\left({Y}\right)\to {D}\in \mathrm{Bnd}\left({Y}\right)$
11 simpr ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {D}\in \mathrm{Bnd}\left({Y}\right)$
12 1 adantr ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {M}\in \mathrm{Met}\left({X}\right)$
13 8 bnd2lem ${⊢}\left({N}\in \mathrm{Met}\left({X}\right)\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {Y}\subseteq {X}$
14 2 13 sylan ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {Y}\subseteq {X}$
15 metres2 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to {{M}↾}_{\left({Y}×{Y}\right)}\in \mathrm{Met}\left({Y}\right)$
16 12 14 15 syl2anc ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {{M}↾}_{\left({Y}×{Y}\right)}\in \mathrm{Met}\left({Y}\right)$
17 7 16 eqeltrid ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {C}\in \mathrm{Met}\left({Y}\right)$
18 4 adantr ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {S}\in {ℝ}^{+}$
19 14 sselda ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge {x}\in {Y}\right)\to {x}\in {X}$
20 14 sselda ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge {y}\in {Y}\right)\to {y}\in {X}$
21 19 20 anim12dan ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to \left({x}\in {X}\wedge {y}\in {X}\right)$
22 6 adantlr ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{M}{y}\le {S}\left({x}{N}{y}\right)$
23 21 22 syldan ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to {x}{M}{y}\le {S}\left({x}{N}{y}\right)$
24 7 oveqi ${⊢}{x}{C}{y}={x}\left({{M}↾}_{\left({Y}×{Y}\right)}\right){y}$
25 ovres ${⊢}\left({x}\in {Y}\wedge {y}\in {Y}\right)\to {x}\left({{M}↾}_{\left({Y}×{Y}\right)}\right){y}={x}{M}{y}$
26 24 25 syl5eq ${⊢}\left({x}\in {Y}\wedge {y}\in {Y}\right)\to {x}{C}{y}={x}{M}{y}$
27 26 adantl ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to {x}{C}{y}={x}{M}{y}$
28 8 oveqi ${⊢}{x}{D}{y}={x}\left({{N}↾}_{\left({Y}×{Y}\right)}\right){y}$
29 ovres ${⊢}\left({x}\in {Y}\wedge {y}\in {Y}\right)\to {x}\left({{N}↾}_{\left({Y}×{Y}\right)}\right){y}={x}{N}{y}$
30 28 29 syl5eq ${⊢}\left({x}\in {Y}\wedge {y}\in {Y}\right)\to {x}{D}{y}={x}{N}{y}$
31 30 adantl ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to {x}{D}{y}={x}{N}{y}$
32 31 oveq2d ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to {S}\left({x}{D}{y}\right)={S}\left({x}{N}{y}\right)$
33 23 27 32 3brtr4d ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to {x}{C}{y}\le {S}\left({x}{D}{y}\right)$
34 11 17 18 33 equivbnd ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {C}\in \mathrm{Bnd}\left({Y}\right)$
35 9 biimpar ${⊢}\left({\phi }\wedge {C}\in \mathrm{Bnd}\left({Y}\right)\right)\to {C}\in \mathrm{TotBnd}\left({Y}\right)$
36 34 35 syldan ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {C}\in \mathrm{TotBnd}\left({Y}\right)$
37 bndmet ${⊢}{D}\in \mathrm{Bnd}\left({Y}\right)\to {D}\in \mathrm{Met}\left({Y}\right)$
38 37 adantl ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {D}\in \mathrm{Met}\left({Y}\right)$
39 3 adantr ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {R}\in {ℝ}^{+}$
40 5 adantlr ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
41 21 40 syldan ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to {x}{N}{y}\le {R}\left({x}{M}{y}\right)$
42 27 oveq2d ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to {R}\left({x}{C}{y}\right)={R}\left({x}{M}{y}\right)$
43 41 31 42 3brtr4d ${⊢}\left(\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\wedge \left({x}\in {Y}\wedge {y}\in {Y}\right)\right)\to {x}{D}{y}\le {R}\left({x}{C}{y}\right)$
44 36 38 39 43 equivtotbnd ${⊢}\left({\phi }\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {D}\in \mathrm{TotBnd}\left({Y}\right)$
45 44 ex ${⊢}{\phi }\to \left({D}\in \mathrm{Bnd}\left({Y}\right)\to {D}\in \mathrm{TotBnd}\left({Y}\right)\right)$
46 10 45 impbid2 ${⊢}{\phi }\to \left({D}\in \mathrm{TotBnd}\left({Y}\right)↔{D}\in \mathrm{Bnd}\left({Y}\right)\right)$