# Metamath Proof Explorer

## Theorem prdsbnd2

Description: If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses prdsbnd.y ${⊢}{Y}={S}{⨉}_{𝑠}{R}$
prdsbnd.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
prdsbnd.v ${⊢}{V}={\mathrm{Base}}_{{R}\left({x}\right)}$
prdsbnd.e ${⊢}{E}={\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left({V}×{V}\right)}$
prdsbnd.d ${⊢}{D}=\mathrm{dist}\left({Y}\right)$
prdsbnd.s ${⊢}{\phi }\to {S}\in {W}$
prdsbnd.i ${⊢}{\phi }\to {I}\in \mathrm{Fin}$
prdsbnd.r ${⊢}{\phi }\to {R}Fn{I}$
prdsbnd2.c ${⊢}{C}={{D}↾}_{\left({A}×{A}\right)}$
prdsbnd2.e ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
prdsbnd2.m ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \left({{E}↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{{E}↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)$
Assertion prdsbnd2 ${⊢}{\phi }\to \left({C}\in \mathrm{TotBnd}\left({A}\right)↔{C}\in \mathrm{Bnd}\left({A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 prdsbnd.y ${⊢}{Y}={S}{⨉}_{𝑠}{R}$
2 prdsbnd.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
3 prdsbnd.v ${⊢}{V}={\mathrm{Base}}_{{R}\left({x}\right)}$
4 prdsbnd.e ${⊢}{E}={\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left({V}×{V}\right)}$
5 prdsbnd.d ${⊢}{D}=\mathrm{dist}\left({Y}\right)$
6 prdsbnd.s ${⊢}{\phi }\to {S}\in {W}$
7 prdsbnd.i ${⊢}{\phi }\to {I}\in \mathrm{Fin}$
8 prdsbnd.r ${⊢}{\phi }\to {R}Fn{I}$
9 prdsbnd2.c ${⊢}{C}={{D}↾}_{\left({A}×{A}\right)}$
10 prdsbnd2.e ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
11 prdsbnd2.m ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \left({{E}↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{{E}↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)$
12 totbndbnd ${⊢}{C}\in \mathrm{TotBnd}\left({A}\right)\to {C}\in \mathrm{Bnd}\left({A}\right)$
13 bndmet ${⊢}{C}\in \mathrm{Bnd}\left({A}\right)\to {C}\in \mathrm{Met}\left({A}\right)$
14 0totbnd ${⊢}{A}=\varnothing \to \left({C}\in \mathrm{TotBnd}\left({A}\right)↔{C}\in \mathrm{Met}\left({A}\right)\right)$
15 13 14 syl5ibr ${⊢}{A}=\varnothing \to \left({C}\in \mathrm{Bnd}\left({A}\right)\to {C}\in \mathrm{TotBnd}\left({A}\right)\right)$
16 15 a1i ${⊢}{\phi }\to \left({A}=\varnothing \to \left({C}\in \mathrm{Bnd}\left({A}\right)\to {C}\in \mathrm{TotBnd}\left({A}\right)\right)\right)$
17 n0 ${⊢}{A}\ne \varnothing ↔\exists {a}\phantom{\rule{.4em}{0ex}}{a}\in {A}$
18 simprr ${⊢}\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\to {C}\in \mathrm{Bnd}\left({A}\right)$
19 eqid ${⊢}{S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
20 eqid ${⊢}{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
21 eqid ${⊢}\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)$
22 fvexd ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {R}\left({x}\right)\in \mathrm{V}$
23 19 20 3 4 21 6 7 22 10 prdsmet ${⊢}{\phi }\to \mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)\in \mathrm{Met}\left({\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}\right)$
24 dffn5 ${⊢}{R}Fn{I}↔{R}=\left({x}\in {I}⟼{R}\left({x}\right)\right)$
25 8 24 sylib ${⊢}{\phi }\to {R}=\left({x}\in {I}⟼{R}\left({x}\right)\right)$
26 25 oveq2d ${⊢}{\phi }\to {S}{⨉}_{𝑠}{R}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
27 1 26 syl5eq ${⊢}{\phi }\to {Y}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
28 27 fveq2d ${⊢}{\phi }\to \mathrm{dist}\left({Y}\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)$
29 5 28 syl5eq ${⊢}{\phi }\to {D}=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)$
30 27 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
31 2 30 syl5eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
32 31 fveq2d ${⊢}{\phi }\to \mathrm{Met}\left({B}\right)=\mathrm{Met}\left({\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}\right)$
33 23 29 32 3eltr4d ${⊢}{\phi }\to {D}\in \mathrm{Met}\left({B}\right)$
34 33 adantr ${⊢}\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\to {D}\in \mathrm{Met}\left({B}\right)$
35 simpr ${⊢}\left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\to {C}\in \mathrm{Bnd}\left({A}\right)$
36 9 bnd2lem ${⊢}\left({D}\in \mathrm{Met}\left({B}\right)\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\to {A}\subseteq {B}$
37 33 35 36 syl2an ${⊢}\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\to {A}\subseteq {B}$
38 simprl ${⊢}\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\to {a}\in {A}$
39 37 38 sseldd ${⊢}\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\to {a}\in {B}$
40 9 ssbnd ${⊢}\left({D}\in \mathrm{Met}\left({B}\right)\wedge {a}\in {B}\right)\to \left({C}\in \mathrm{Bnd}\left({A}\right)↔\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}{A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)$
41 34 39 40 syl2anc ${⊢}\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\to \left({C}\in \mathrm{Bnd}\left({A}\right)↔\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}{A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)$
42 18 41 mpbid ${⊢}\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}{A}\subseteq {a}\mathrm{ball}\left({D}\right){r}$
43 simprr ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}$
44 xpss12 ${⊢}\left({A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\to {A}×{A}\subseteq \left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)$
45 43 43 44 syl2anc ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {A}×{A}\subseteq \left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)$
46 45 resabs1d ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {\left({{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}\right)↾}_{\left({A}×{A}\right)}={{D}↾}_{\left({A}×{A}\right)}$
47 46 9 syl6eqr ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {\left({{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}\right)↾}_{\left({A}×{A}\right)}={C}$
48 simpll ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {\phi }$
49 39 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {a}\in {B}$
50 simprl ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {r}\in ℝ$
51 38 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {a}\in {A}$
52 43 51 sseldd ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {a}\in \left({a}\mathrm{ball}\left({D}\right){r}\right)$
53 52 ne0d ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {a}\mathrm{ball}\left({D}\right){r}\ne \varnothing$
54 33 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {D}\in \mathrm{Met}\left({B}\right)$
55 metxmet ${⊢}{D}\in \mathrm{Met}\left({B}\right)\to {D}\in \mathrm{\infty Met}\left({B}\right)$
56 54 55 syl ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {D}\in \mathrm{\infty Met}\left({B}\right)$
57 50 rexrd ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {r}\in {ℝ}^{*}$
58 xbln0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({B}\right)\wedge {a}\in {B}\wedge {r}\in {ℝ}^{*}\right)\to \left({a}\mathrm{ball}\left({D}\right){r}\ne \varnothing ↔0<{r}\right)$
59 56 49 57 58 syl3anc ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to \left({a}\mathrm{ball}\left({D}\right){r}\ne \varnothing ↔0<{r}\right)$
60 53 59 mpbid ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to 0<{r}$
61 50 60 elrpd ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {r}\in {ℝ}^{+}$
62 eqid ${⊢}{S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)={S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)$
63 eqid ${⊢}{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)}$
64 eqid ${⊢}{\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}={\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}$
65 eqid ${⊢}{\mathrm{dist}\left(\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}×{\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}\right)}={\mathrm{dist}\left(\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}×{\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}\right)}$
66 eqid ${⊢}\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)$
67 6 adantr ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {S}\in {W}$
68 7 adantr ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {I}\in \mathrm{Fin}$
69 ovex ${⊢}{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\in \mathrm{V}$
70 fveq2 ${⊢}{y}={x}\to {R}\left({y}\right)={R}\left({x}\right)$
71 2fveq3 ${⊢}{y}={x}\to \mathrm{dist}\left({R}\left({y}\right)\right)=\mathrm{dist}\left({R}\left({x}\right)\right)$
72 2fveq3 ${⊢}{y}={x}\to {\mathrm{Base}}_{{R}\left({y}\right)}={\mathrm{Base}}_{{R}\left({x}\right)}$
73 72 3 syl6eqr ${⊢}{y}={x}\to {\mathrm{Base}}_{{R}\left({y}\right)}={V}$
74 73 sqxpeqd ${⊢}{y}={x}\to {\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}={V}×{V}$
75 71 74 reseq12d ${⊢}{y}={x}\to {\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}={\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left({V}×{V}\right)}$
76 75 4 syl6eqr ${⊢}{y}={x}\to {\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}={E}$
77 76 fveq2d ${⊢}{y}={x}\to \mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right)=\mathrm{ball}\left({E}\right)$
78 fveq2 ${⊢}{y}={x}\to {a}\left({y}\right)={a}\left({x}\right)$
79 eqidd ${⊢}{y}={x}\to {r}={r}$
80 77 78 79 oveq123d ${⊢}{y}={x}\to {a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}$
81 70 80 oveq12d ${⊢}{y}={x}\to {R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)={R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
82 81 cbvmptv ${⊢}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)=\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
83 69 82 fnmpti ${⊢}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)Fn{I}$
84 83 a1i ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)Fn{I}$
85 10 adantlr ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
86 metxmet ${⊢}{E}\in \mathrm{Met}\left({V}\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
87 85 86 syl ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
88 22 ralrimiva ${⊢}{\phi }\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{R}\left({x}\right)\in \mathrm{V}$
89 88 adantr ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{R}\left({x}\right)\in \mathrm{V}$
90 simprl ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {a}\in {B}$
91 31 adantr ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
92 90 91 eleqtrd ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {a}\in {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
93 19 20 67 68 89 3 92 prdsbascl ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{a}\left({x}\right)\in {V}$
94 93 r19.21bi ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {a}\left({x}\right)\in {V}$
95 simplrr ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {r}\in {ℝ}^{+}$
96 95 rpred ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {r}\in ℝ$
97 blbnd ${⊢}\left({E}\in \mathrm{\infty Met}\left({V}\right)\wedge {a}\left({x}\right)\in {V}\wedge {r}\in ℝ\right)\to {{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{Bnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
98 87 94 96 97 syl3anc ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{Bnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
99 ovex ${⊢}{a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\in \mathrm{V}$
100 xpeq12 ${⊢}\left({y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\wedge {y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\to {y}×{y}=\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
101 100 anidms ${⊢}{y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\to {y}×{y}=\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
102 101 reseq2d ${⊢}{y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\to {{E}↾}_{\left({y}×{y}\right)}={{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
103 fveq2 ${⊢}{y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\to \mathrm{TotBnd}\left({y}\right)=\mathrm{TotBnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
104 102 103 eleq12d ${⊢}{y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\to \left({{E}↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
105 fveq2 ${⊢}{y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\to \mathrm{Bnd}\left({y}\right)=\mathrm{Bnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
106 102 105 eleq12d ${⊢}{y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\to \left({{E}↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)↔{{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{Bnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
107 104 106 bibi12d ${⊢}{y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\to \left(\left({{E}↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{{E}↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)↔\left({{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)↔{{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{Bnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
108 107 imbi2d ${⊢}{y}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\to \left(\left(\left({\phi }\wedge {x}\in {I}\right)\to \left({{E}↾}_{\left({y}×{y}\right)}\in \mathrm{TotBnd}\left({y}\right)↔{{E}↾}_{\left({y}×{y}\right)}\in \mathrm{Bnd}\left({y}\right)\right)\right)↔\left(\left({\phi }\wedge {x}\in {I}\right)\to \left({{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)↔{{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{Bnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)$
109 99 108 11 vtocl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \left({{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)↔{{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{Bnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
110 109 adantlr ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to \left({{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)↔{{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{Bnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
111 98 110 mpbird ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
112 eqid ${⊢}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)=\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)$
113 81 112 69 fvmpt ${⊢}{x}\in {I}\to \left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)={R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
114 113 adantl ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to \left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)={R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
115 114 fveq2d ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to \mathrm{dist}\left(\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)\right)=\mathrm{dist}\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
116 eqid ${⊢}{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)={R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
117 eqid ${⊢}\mathrm{dist}\left({R}\left({x}\right)\right)=\mathrm{dist}\left({R}\left({x}\right)\right)$
118 116 117 ressds ${⊢}{a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\in \mathrm{V}\to \mathrm{dist}\left({R}\left({x}\right)\right)=\mathrm{dist}\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
119 99 118 ax-mp ${⊢}\mathrm{dist}\left({R}\left({x}\right)\right)=\mathrm{dist}\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
120 115 119 syl6eqr ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to \mathrm{dist}\left(\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)\right)=\mathrm{dist}\left({R}\left({x}\right)\right)$
121 114 fveq2d ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}={\mathrm{Base}}_{\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
122 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
123 122 ad2antll ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {r}\in {ℝ}^{*}$
124 123 adantr ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {r}\in {ℝ}^{*}$
125 blssm ${⊢}\left({E}\in \mathrm{\infty Met}\left({V}\right)\wedge {a}\left({x}\right)\in {V}\wedge {r}\in {ℝ}^{*}\right)\to {a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\subseteq {V}$
126 87 94 124 125 syl3anc ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\subseteq {V}$
127 116 3 ressbas2 ${⊢}{a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\subseteq {V}\to {a}\left({x}\right)\mathrm{ball}\left({E}\right){r}={\mathrm{Base}}_{\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
128 126 127 syl ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {a}\left({x}\right)\mathrm{ball}\left({E}\right){r}={\mathrm{Base}}_{\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
129 121 128 eqtr4d ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}={a}\left({x}\right)\mathrm{ball}\left({E}\right){r}$
130 129 sqxpeqd ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}×{\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}=\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
131 120 130 reseq12d ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {\mathrm{dist}\left(\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}×{\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}\right)}={\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
132 4 reseq1i ${⊢}{{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}={\left({\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left({V}×{V}\right)}\right)↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
133 xpss12 ${⊢}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\subseteq {V}\wedge {a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\subseteq {V}\right)\to \left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\subseteq {V}×{V}$
134 126 126 133 syl2anc ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to \left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\subseteq {V}×{V}$
135 134 resabs1d ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {\left({\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left({V}×{V}\right)}\right)↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}={\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
136 132 135 syl5eq ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}={\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
137 131 136 eqtr4d ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {\mathrm{dist}\left(\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}×{\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}\right)}={{E}↾}_{\left(\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)×\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
138 129 fveq2d ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to \mathrm{TotBnd}\left({\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}\right)=\mathrm{TotBnd}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
139 111 137 138 3eltr4d ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {\mathrm{dist}\left(\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)\right)↾}_{\left({\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}×{\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}\right)}\in \mathrm{TotBnd}\left({\mathrm{Base}}_{\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\left({x}\right)}\right)$
140 62 63 64 65 66 67 68 84 139 prdstotbnd ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)\in \mathrm{TotBnd}\left({\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)}\right)$
141 27 adantr ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {Y}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
142 eqidd ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
143 eqid ${⊢}{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}$
144 82 oveq2i ${⊢}{S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
145 144 fveq2i ${⊢}\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
146 fvexd ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {R}\left({x}\right)\in \mathrm{V}$
147 99 a1i ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\in \mathrm{V}$
148 141 142 143 5 145 67 67 68 146 147 ressprdsds ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)={{D}↾}_{\left({\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}×{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}\right)}$
149 128 ixpeq2dva ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \underset{{x}\in {I}}{⨉}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
150 70 cbvmptv ${⊢}\left({y}\in {I}⟼{R}\left({y}\right)\right)=\left({x}\in {I}⟼{R}\left({x}\right)\right)$
151 150 oveq2i ${⊢}{S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
152 27 151 syl6eqr ${⊢}{\phi }\to {Y}={S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)$
153 152 fveq2d ${⊢}{\phi }\to \mathrm{dist}\left({Y}\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)$
154 5 153 syl5eq ${⊢}{\phi }\to {D}=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)$
155 154 fveq2d ${⊢}{\phi }\to \mathrm{ball}\left({D}\right)=\mathrm{ball}\left(\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)\right)$
156 155 oveqdr ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {a}\mathrm{ball}\left({D}\right){r}={a}\mathrm{ball}\left(\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)\right){r}$
157 eqid ${⊢}{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
158 eqid ${⊢}\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)$
159 152 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
160 2 159 syl5eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
161 160 adantr ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
162 90 161 eleqtrd ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {a}\in {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
163 rpgt0 ${⊢}{r}\in {ℝ}^{+}\to 0<{r}$
164 163 ad2antll ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to 0<{r}$
165 151 157 3 4 158 67 68 146 87 162 123 164 prdsbl ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {a}\mathrm{ball}\left(\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)\right){r}=\underset{{x}\in {I}}{⨉}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
166 156 165 eqtrd ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {a}\mathrm{ball}\left({D}\right){r}=\underset{{x}\in {I}}{⨉}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
167 eqid ${⊢}{S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
168 69 a1i ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\in \mathrm{V}$
169 168 ralrimiva ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\in \mathrm{V}$
170 eqid ${⊢}{\mathrm{Base}}_{\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}={\mathrm{Base}}_{\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
171 167 143 67 68 169 170 prdsbas3 ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{\left({R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)}$
172 149 166 171 3eqtr4rd ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}={a}\mathrm{ball}\left({D}\right){r}$
173 172 sqxpeqd ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}×{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}=\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)$
174 173 reseq2d ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {{D}↾}_{\left({\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}×{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}\right)}={{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}$
175 148 174 eqtrd ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)={{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}$
176 144 fveq2i ${⊢}{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right){↾}_{𝑠}\left({a}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)}$
177 176 172 syl5eq ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)}={a}\mathrm{ball}\left({D}\right){r}$
178 177 fveq2d ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to \mathrm{TotBnd}\left({\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right){↾}_{𝑠}\left({a}\left({y}\right)\mathrm{ball}\left({\mathrm{dist}\left({R}\left({y}\right)\right)↾}_{\left({\mathrm{Base}}_{{R}\left({y}\right)}×{\mathrm{Base}}_{{R}\left({y}\right)}\right)}\right){r}\right)\right)\right)}\right)=\mathrm{TotBnd}\left({a}\mathrm{ball}\left({D}\right){r}\right)$
179 140 175 178 3eltr3d ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\mathrm{ball}\left({D}\right){r}\right)$
180 48 49 61 179 syl12anc ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\mathrm{ball}\left({D}\right){r}\right)$
181 totbndss ${⊢}\left({{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}\in \mathrm{TotBnd}\left({a}\mathrm{ball}\left({D}\right){r}\right)\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\to {\left({{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}\right)↾}_{\left({A}×{A}\right)}\in \mathrm{TotBnd}\left({A}\right)$
182 180 43 181 syl2anc ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {\left({{D}↾}_{\left(\left({a}\mathrm{ball}\left({D}\right){r}\right)×\left({a}\mathrm{ball}\left({D}\right){r}\right)\right)}\right)↾}_{\left({A}×{A}\right)}\in \mathrm{TotBnd}\left({A}\right)$
183 47 182 eqeltrrd ${⊢}\left(\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\wedge \left({r}\in ℝ\wedge {A}\subseteq {a}\mathrm{ball}\left({D}\right){r}\right)\right)\to {C}\in \mathrm{TotBnd}\left({A}\right)$
184 42 183 rexlimddv ${⊢}\left({\phi }\wedge \left({a}\in {A}\wedge {C}\in \mathrm{Bnd}\left({A}\right)\right)\right)\to {C}\in \mathrm{TotBnd}\left({A}\right)$
185 184 exp32 ${⊢}{\phi }\to \left({a}\in {A}\to \left({C}\in \mathrm{Bnd}\left({A}\right)\to {C}\in \mathrm{TotBnd}\left({A}\right)\right)\right)$
186 185 exlimdv ${⊢}{\phi }\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}{a}\in {A}\to \left({C}\in \mathrm{Bnd}\left({A}\right)\to {C}\in \mathrm{TotBnd}\left({A}\right)\right)\right)$
187 17 186 syl5bi ${⊢}{\phi }\to \left({A}\ne \varnothing \to \left({C}\in \mathrm{Bnd}\left({A}\right)\to {C}\in \mathrm{TotBnd}\left({A}\right)\right)\right)$
188 16 187 pm2.61dne ${⊢}{\phi }\to \left({C}\in \mathrm{Bnd}\left({A}\right)\to {C}\in \mathrm{TotBnd}\left({A}\right)\right)$
189 12 188 impbid2 ${⊢}{\phi }\to \left({C}\in \mathrm{TotBnd}\left({A}\right)↔{C}\in \mathrm{Bnd}\left({A}\right)\right)$