# Metamath Proof Explorer

## Theorem prdstotbnd

Description: The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-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}$
prdstotbnd.m ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{TotBnd}\left({V}\right)$
Assertion prdstotbnd ${⊢}{\phi }\to {D}\in \mathrm{TotBnd}\left({B}\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 prdstotbnd.m ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{TotBnd}\left({V}\right)$
10 eqid ${⊢}{S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
11 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)}$
12 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)$
13 fvexd ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {R}\left({x}\right)\in \mathrm{V}$
14 totbndmet ${⊢}{E}\in \mathrm{TotBnd}\left({V}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
15 9 14 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
16 10 11 3 4 12 6 7 13 15 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)$
17 dffn5 ${⊢}{R}Fn{I}↔{R}=\left({x}\in {I}⟼{R}\left({x}\right)\right)$
18 8 17 sylib ${⊢}{\phi }\to {R}=\left({x}\in {I}⟼{R}\left({x}\right)\right)$
19 18 oveq2d ${⊢}{\phi }\to {S}{⨉}_{𝑠}{R}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
20 1 19 syl5eq ${⊢}{\phi }\to {Y}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
21 20 fveq2d ${⊢}{\phi }\to \mathrm{dist}\left({Y}\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)$
22 5 21 syl5eq ${⊢}{\phi }\to {D}=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)$
23 20 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
24 2 23 syl5eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
25 24 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)$
26 16 22 25 3eltr4d ${⊢}{\phi }\to {D}\in \mathrm{Met}\left({B}\right)$
27 7 adantr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to {I}\in \mathrm{Fin}$
28 istotbnd3 ${⊢}{E}\in \mathrm{TotBnd}\left({V}\right)↔\left({E}\in \mathrm{Met}\left({V}\right)\wedge \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)$
29 28 simprbi ${⊢}{E}\in \mathrm{TotBnd}\left({V}\right)\to \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}$
30 9 29 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}$
31 30 r19.21bi ${⊢}\left(\left({\phi }\wedge {x}\in {I}\right)\wedge {r}\in {ℝ}^{+}\right)\to \exists {w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}$
32 df-rex ${⊢}\exists {w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)$
33 rexv ${⊢}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)$
34 32 33 bitr4i ${⊢}\exists {w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}↔\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)$
35 31 34 sylib ${⊢}\left(\left({\phi }\wedge {x}\in {I}\right)\wedge {r}\in {ℝ}^{+}\right)\to \exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)$
36 35 an32s ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {I}\right)\to \exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)$
37 36 ralrimiva ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)$
38 eleq1 ${⊢}{w}={f}\left({x}\right)\to \left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)↔{f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\right)$
39 iuneq1 ${⊢}{w}={f}\left({x}\right)\to \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)=\bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)$
40 39 eqeq1d ${⊢}{w}={f}\left({x}\right)\to \left(\bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}↔\bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)$
41 38 40 anbi12d ${⊢}{w}={f}\left({x}\right)\to \left(\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)↔\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)$
42 41 ac6sfi ${⊢}\left({I}\in \mathrm{Fin}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({w}\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {w}}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)$
43 27 37 42 syl2anc ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)$
44 elfpw ${⊢}{f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)↔\left({f}\left({x}\right)\subseteq {V}\wedge {f}\left({x}\right)\in \mathrm{Fin}\right)$
45 44 simplbi ${⊢}{f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\to {f}\left({x}\right)\subseteq {V}$
46 45 adantr ${⊢}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\to {f}\left({x}\right)\subseteq {V}$
47 46 ralimi ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\subseteq {V}$
48 47 ad2antll ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\subseteq {V}$
49 ss2ixp ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\subseteq {V}\to \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\subseteq \underset{{x}\in {I}}{⨉}{V}$
50 48 49 syl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\subseteq \underset{{x}\in {I}}{⨉}{V}$
51 fnfi ${⊢}\left({R}Fn{I}\wedge {I}\in \mathrm{Fin}\right)\to {R}\in \mathrm{Fin}$
52 8 7 51 syl2anc ${⊢}{\phi }\to {R}\in \mathrm{Fin}$
53 fndm ${⊢}{R}Fn{I}\to \mathrm{dom}{R}={I}$
54 8 53 syl ${⊢}{\phi }\to \mathrm{dom}{R}={I}$
55 1 6 52 2 54 prdsbas ${⊢}{\phi }\to {B}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
56 3 rgenw ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{V}={\mathrm{Base}}_{{R}\left({x}\right)}$
57 ixpeq2 ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{V}={\mathrm{Base}}_{{R}\left({x}\right)}\to \underset{{x}\in {I}}{⨉}{V}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
58 56 57 ax-mp ${⊢}\underset{{x}\in {I}}{⨉}{V}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
59 55 58 syl6eqr ${⊢}{\phi }\to {B}=\underset{{x}\in {I}}{⨉}{V}$
60 59 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to {B}=\underset{{x}\in {I}}{⨉}{V}$
61 50 60 sseqtrrd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\subseteq {B}$
62 27 adantr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to {I}\in \mathrm{Fin}$
63 44 simprbi ${⊢}{f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\to {f}\left({x}\right)\in \mathrm{Fin}$
64 63 adantr ${⊢}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\to {f}\left({x}\right)\in \mathrm{Fin}$
65 64 ralimi ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \mathrm{Fin}$
66 65 ad2antll ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \mathrm{Fin}$
67 ixpfi ${⊢}\left({I}\in \mathrm{Fin}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \mathrm{Fin}\right)\to \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\in \mathrm{Fin}$
68 62 66 67 syl2anc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\in \mathrm{Fin}$
69 elfpw ${⊢}\underset{{x}\in {I}}{⨉}{f}\left({x}\right)\in \left(𝒫{B}\cap \mathrm{Fin}\right)↔\left(\underset{{x}\in {I}}{⨉}{f}\left({x}\right)\subseteq {B}\wedge \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\in \mathrm{Fin}\right)$
70 61 68 69 sylanbrc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\in \left(𝒫{B}\cap \mathrm{Fin}\right)$
71 metxmet ${⊢}{D}\in \mathrm{Met}\left({B}\right)\to {D}\in \mathrm{\infty Met}\left({B}\right)$
72 26 71 syl ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({B}\right)$
73 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
74 blssm ${⊢}\left({D}\in \mathrm{\infty Met}\left({B}\right)\wedge {y}\in {B}\wedge {r}\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({D}\right){r}\subseteq {B}$
75 74 3expa ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({B}\right)\wedge {y}\in {B}\right)\wedge {r}\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({D}\right){r}\subseteq {B}$
76 75 an32s ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({B}\right)\wedge {r}\in {ℝ}^{*}\right)\wedge {y}\in {B}\right)\to {y}\mathrm{ball}\left({D}\right){r}\subseteq {B}$
77 76 ralrimiva ${⊢}\left({D}\in \mathrm{\infty Met}\left({B}\right)\wedge {r}\in {ℝ}^{*}\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {B}$
78 72 73 77 syl2an ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {B}$
79 78 adantr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {B}$
80 ssralv ${⊢}\underset{{x}\in {I}}{⨉}{f}\left({x}\right)\subseteq {B}\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {B}\to \forall {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {B}\right)$
81 61 79 80 sylc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \forall {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {B}$
82 iunss ${⊢}\bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)\subseteq {B}↔\forall {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {B}$
83 81 82 sylibr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)\subseteq {B}$
84 62 adantr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to {I}\in \mathrm{Fin}$
85 60 eleq2d ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \left({g}\in {B}↔{g}\in \underset{{x}\in {I}}{⨉}{V}\right)$
86 vex ${⊢}{g}\in \mathrm{V}$
87 86 elixp ${⊢}{g}\in \underset{{x}\in {I}}{⨉}{V}↔\left({g}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {V}\right)$
88 87 simprbi ${⊢}{g}\in \underset{{x}\in {I}}{⨉}{V}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {V}$
89 df-rex ${⊢}\exists {z}\in {f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)$
90 eliun ${⊢}{g}\left({x}\right)\in \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)↔\exists {z}\in {f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)$
91 rexv ${⊢}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)$
92 89 90 91 3bitr4i ${⊢}{g}\left({x}\right)\in \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)↔\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)$
93 eleq2 ${⊢}\bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\to \left({g}\left({x}\right)\in \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)↔{g}\left({x}\right)\in {V}\right)$
94 92 93 syl5bbr ${⊢}\bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\to \left(\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)↔{g}\left({x}\right)\in {V}\right)$
95 94 biimprd ${⊢}\bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\to \left({g}\left({x}\right)\in {V}\to \exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
96 95 adantl ${⊢}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\to \left({g}\left({x}\right)\in {V}\to \exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
97 96 ral2imi ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {V}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
98 97 ad2antll ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {V}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
99 88 98 syl5 ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \left({g}\in \underset{{x}\in {I}}{⨉}{V}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
100 85 99 sylbid ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \left({g}\in {B}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
101 100 imp ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)$
102 eleq1 ${⊢}{z}={y}\left({x}\right)\to \left({z}\in {f}\left({x}\right)↔{y}\left({x}\right)\in {f}\left({x}\right)\right)$
103 oveq1 ${⊢}{z}={y}\left({x}\right)\to {z}\mathrm{ball}\left({E}\right){r}={y}\left({x}\right)\mathrm{ball}\left({E}\right){r}$
104 103 eleq2d ${⊢}{z}={y}\left({x}\right)\to \left({g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)↔{g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
105 102 104 anbi12d ${⊢}{z}={y}\left({x}\right)\to \left(\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)↔\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
106 105 ac6sfi ${⊢}\left({I}\in \mathrm{Fin}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({z}\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({z}\mathrm{ball}\left({E}\right){r}\right)\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
107 84 101 106 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)$
108 ffn ${⊢}{y}:{I}⟶\mathrm{V}\to {y}Fn{I}$
109 simpl ${⊢}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\to {y}\left({x}\right)\in {f}\left({x}\right)$
110 109 ralimi ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({x}\right)\in {f}\left({x}\right)$
111 108 110 anim12i ${⊢}\left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\to \left({y}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({x}\right)\in {f}\left({x}\right)\right)$
112 vex ${⊢}{y}\in \mathrm{V}$
113 112 elixp ${⊢}{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)↔\left({y}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({x}\right)\in {f}\left({x}\right)\right)$
114 111 113 sylibr ${⊢}\left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\to {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)$
115 114 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)$
116 85 biimpa ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to {g}\in \underset{{x}\in {I}}{⨉}{V}$
117 ixpfn ${⊢}{g}\in \underset{{x}\in {I}}{⨉}{V}\to {g}Fn{I}$
118 116 117 syl ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to {g}Fn{I}$
119 118 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {g}Fn{I}$
120 simpr ${⊢}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\to {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
121 120 ralimi ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
122 121 ad2antll ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
123 86 elixp ${⊢}{g}\in \underset{{x}\in {I}}{⨉}\left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)↔\left({g}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)$
124 119 122 123 sylanbrc ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {g}\in \underset{{x}\in {I}}{⨉}\left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
125 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {\phi }$
126 50 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\subseteq \underset{{x}\in {I}}{⨉}{V}$
127 126 115 sseldd ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {y}\in \underset{{x}\in {I}}{⨉}{V}$
128 125 59 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {B}=\underset{{x}\in {I}}{⨉}{V}$
129 127 128 eleqtrrd ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {y}\in {B}$
130 simp-4r ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {r}\in {ℝ}^{+}$
131 fveq2 ${⊢}{y}={x}\to {R}\left({y}\right)={R}\left({x}\right)$
132 131 cbvmptv ${⊢}\left({y}\in {I}⟼{R}\left({y}\right)\right)=\left({x}\in {I}⟼{R}\left({x}\right)\right)$
133 132 oveq2i ${⊢}{S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
134 20 133 syl6eqr ${⊢}{\phi }\to {Y}={S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)$
135 134 fveq2d ${⊢}{\phi }\to \mathrm{dist}\left({Y}\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)$
136 5 135 syl5eq ${⊢}{\phi }\to {D}=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)$
137 136 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)$
138 137 oveqdr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\mathrm{ball}\left({D}\right){r}={y}\mathrm{ball}\left(\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)\right){r}$
139 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)}$
140 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)$
141 6 adantr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {S}\in {W}$
142 7 adantr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {I}\in \mathrm{Fin}$
143 fvexd ${⊢}\left(\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {R}\left({x}\right)\in \mathrm{V}$
144 metxmet ${⊢}{E}\in \mathrm{Met}\left({V}\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
145 15 144 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
146 145 adantlr ${⊢}\left(\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\wedge {x}\in {I}\right)\to {E}\in \mathrm{\infty Met}\left({V}\right)$
147 simprl ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\in {B}$
148 134 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
149 2 148 syl5eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
150 149 adantr ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
151 147 150 eleqtrd ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\in {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)}$
152 73 ad2antll ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {r}\in {ℝ}^{*}$
153 rpgt0 ${⊢}{r}\in {ℝ}^{+}\to 0<{r}$
154 153 ad2antll ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to 0<{r}$
155 133 139 3 4 140 141 142 143 146 151 152 154 prdsbl ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\mathrm{ball}\left(\mathrm{dist}\left({S}{⨉}_{𝑠}\left({y}\in {I}⟼{R}\left({y}\right)\right)\right)\right){r}=\underset{{x}\in {I}}{⨉}\left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
156 138 155 eqtrd ${⊢}\left({\phi }\wedge \left({y}\in {B}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\mathrm{ball}\left({D}\right){r}=\underset{{x}\in {I}}{⨉}\left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
157 125 129 130 156 syl12anc ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {y}\mathrm{ball}\left({D}\right){r}=\underset{{x}\in {I}}{⨉}\left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)$
158 124 157 eleqtrrd ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to {g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)$
159 115 158 jca ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\wedge \left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\right)\to \left({y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\wedge {g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\right)$
160 159 ex ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to \left(\left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\to \left({y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\wedge {g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\right)\right)$
161 160 eximdv ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\wedge {g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\right)\right)$
162 df-rex ${⊢}\exists {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\wedge {g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\right)$
163 161 162 syl6ibr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({y}\left({x}\right)\in {f}\left({x}\right)\wedge {g}\left({x}\right)\in \left({y}\left({x}\right)\mathrm{ball}\left({E}\right){r}\right)\right)\right)\to \exists {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\right)$
164 107 163 mpd ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\wedge {g}\in {B}\right)\to \exists {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)$
165 164 ex ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \left({g}\in {B}\to \exists {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\right)$
166 eliun ${⊢}{g}\in \bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)↔\exists {y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)\phantom{\rule{.4em}{0ex}}{g}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)$
167 165 166 syl6ibr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \left({g}\in {B}\to {g}\in \bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)\right)$
168 167 ssrdv ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to {B}\subseteq \bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)$
169 83 168 eqssd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}$
170 iuneq1 ${⊢}{v}=\underset{{x}\in {I}}{⨉}{f}\left({x}\right)\to \bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({D}\right){r}\right)=\bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)$
171 170 eqeq1d ${⊢}{v}=\underset{{x}\in {I}}{⨉}{f}\left({x}\right)\to \left(\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}↔\bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}\right)$
172 171 rspcev ${⊢}\left(\underset{{x}\in {I}}{⨉}{f}\left({x}\right)\in \left(𝒫{B}\cap \mathrm{Fin}\right)\wedge \bigcup _{{y}\in \underset{{x}\in {I}}{⨉}{f}\left({x}\right)}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}\right)\to \exists {v}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}$
173 70 169 172 syl2anc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({f}:{I}⟶\mathrm{V}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left(𝒫{V}\cap \mathrm{Fin}\right)\wedge \bigcup _{{z}\in {f}\left({x}\right)}\left({z}\mathrm{ball}\left({E}\right){r}\right)={V}\right)\right)\right)\to \exists {v}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}$
174 43 173 exlimddv ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \exists {v}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}$
175 174 ralrimiva ${⊢}{\phi }\to \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}$
176 istotbnd3 ${⊢}{D}\in \mathrm{TotBnd}\left({B}\right)↔\left({D}\in \mathrm{Met}\left({B}\right)\wedge \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({D}\right){r}\right)={B}\right)$
177 26 175 176 sylanbrc ${⊢}{\phi }\to {D}\in \mathrm{TotBnd}\left({B}\right)$