# Metamath Proof Explorer

## Theorem sstotbnd2

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 ${⊢}{N}={{M}↾}_{\left({Y}×{Y}\right)}$
Assertion sstotbnd2 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({N}\in \mathrm{TotBnd}\left({Y}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$

### Proof

Step Hyp Ref Expression
1 sstotbnd.2 ${⊢}{N}={{M}↾}_{\left({Y}×{Y}\right)}$
2 metres2 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to {{M}↾}_{\left({Y}×{Y}\right)}\in \mathrm{Met}\left({Y}\right)$
3 1 2 eqeltrid ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to {N}\in \mathrm{Met}\left({Y}\right)$
4 istotbnd3 ${⊢}{N}\in \mathrm{TotBnd}\left({Y}\right)↔\left({N}\in \mathrm{Met}\left({Y}\right)\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)$
5 4 baib ${⊢}{N}\in \mathrm{Met}\left({Y}\right)\to \left({N}\in \mathrm{TotBnd}\left({Y}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)$
6 3 5 syl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({N}\in \mathrm{TotBnd}\left({Y}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)$
7 simpllr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to {Y}\subseteq {X}$
8 7 sspwd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to 𝒫{Y}\subseteq 𝒫{X}$
9 8 ssrind ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to 𝒫{Y}\cap \mathrm{Fin}\subseteq 𝒫{X}\cap \mathrm{Fin}$
10 simprl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)$
11 9 10 sseldd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)$
12 simprr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}$
13 metxmet ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
14 13 ad4antr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
15 elfpw ${⊢}{v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)↔\left({v}\subseteq {Y}\wedge {v}\in \mathrm{Fin}\right)$
16 15 simplbi ${⊢}{v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\to {v}\subseteq {Y}$
17 16 adantl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\to {v}\subseteq {Y}$
18 17 sselda ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {x}\in {Y}$
19 simp-4r ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {Y}\subseteq {X}$
20 sseqin2 ${⊢}{Y}\subseteq {X}↔{X}\cap {Y}={Y}$
21 19 20 sylib ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {X}\cap {Y}={Y}$
22 18 21 eleqtrrd ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {x}\in \left({X}\cap {Y}\right)$
23 simpllr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {d}\in {ℝ}^{+}$
24 23 rpxrd ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {d}\in {ℝ}^{*}$
25 1 blres ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in \left({X}\cap {Y}\right)\wedge {d}\in {ℝ}^{*}\right)\to {x}\mathrm{ball}\left({N}\right){d}=\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}$
26 14 22 24 25 syl3anc ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {x}\mathrm{ball}\left({N}\right){d}=\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}$
27 inss1 ${⊢}\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\subseteq {x}\mathrm{ball}\left({M}\right){d}$
28 26 27 eqsstrdi ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\wedge {x}\in {v}\right)\to {x}\mathrm{ball}\left({N}\right){d}\subseteq {x}\mathrm{ball}\left({M}\right){d}$
29 28 ralrimiva ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\to \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({N}\right){d}\subseteq {x}\mathrm{ball}\left({M}\right){d}$
30 ss2iun ${⊢}\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({N}\right){d}\subseteq {x}\mathrm{ball}\left({M}\right){d}\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
31 29 30 syl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
32 31 adantrr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
33 12 32 eqsstrrd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
34 11 33 jca ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\right)\to \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
35 34 ex ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\to \left(\left({v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\right)\to \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)$
36 35 reximdv2 ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {d}\in {ℝ}^{+}\right)\to \left(\exists {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
37 36 ralimdva ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({N}\right){d}\right)={Y}\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
38 6 37 sylbid ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({N}\in \mathrm{TotBnd}\left({Y}\right)\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
39 simpr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\to {c}\in {ℝ}^{+}$
40 39 rphalfcld ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\to \frac{{c}}{2}\in {ℝ}^{+}$
41 oveq2 ${⊢}{d}=\frac{{c}}{2}\to {x}\mathrm{ball}\left({M}\right){d}={x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)$
42 41 iuneq2d ${⊢}{d}=\frac{{c}}{2}\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
43 42 sseq2d ${⊢}{d}=\frac{{c}}{2}\to \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
44 43 rexbidv ${⊢}{d}=\frac{{c}}{2}\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
45 44 rspcv ${⊢}\frac{{c}}{2}\in {ℝ}^{+}\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
46 40 45 syl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
47 elfpw ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)↔\left({v}\subseteq {X}\wedge {v}\in \mathrm{Fin}\right)$
48 47 simprbi ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {v}\in \mathrm{Fin}$
49 48 ad2antrl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to {v}\in \mathrm{Fin}$
50 ssrab2 ${⊢}\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\subseteq {v}$
51 ssfi ${⊢}\left({v}\in \mathrm{Fin}\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\subseteq {v}\right)\to \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}$
52 49 50 51 sylancl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}$
53 oveq1 ${⊢}{x}={y}\to {x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)={y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)$
54 53 ineq1d ${⊢}{x}={y}\to \left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}=\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}$
55 incom ${⊢}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}={Y}\cap \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
56 54 55 syl6eq ${⊢}{x}={y}\to \left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}={Y}\cap \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
57 dfin5 ${⊢}{Y}\cap \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)=\left\{{z}\in {Y}|{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right\}$
58 56 57 syl6eq ${⊢}{x}={y}\to \left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}=\left\{{z}\in {Y}|{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right\}$
59 58 neeq1d ${⊢}{x}={y}\to \left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing ↔\left\{{z}\in {Y}|{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right\}\ne \varnothing \right)$
60 rabn0 ${⊢}\left\{{z}\in {Y}|{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right\}\ne \varnothing ↔\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
61 59 60 syl6bb ${⊢}{x}={y}\to \left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing ↔\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
62 61 elrab ${⊢}{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}↔\left({y}\in {v}\wedge \exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
63 62 simprbi ${⊢}{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\to \exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
64 63 rgen ${⊢}\forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
65 eleq1 ${⊢}{z}={f}\left({y}\right)\to \left({z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)↔{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
66 65 ac6sfi ${⊢}\left(\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{z}\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
67 52 64 66 sylancl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
68 fdm ${⊢}{f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\to \mathrm{dom}{f}=\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}$
69 68 ad2antrl ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \mathrm{dom}{f}=\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}$
70 69 50 eqsstrdi ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \mathrm{dom}{f}\subseteq {v}$
71 simprl ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to {f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}$
72 69 feq2d ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \left({f}:\mathrm{dom}{f}⟶{Y}↔{f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\right)$
73 71 72 mpbird ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to {f}:\mathrm{dom}{f}⟶{Y}$
74 simprr ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
75 ffn ${⊢}{f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\to {f}Fn\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}$
76 elpreima ${⊢}{f}Fn\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\to \left({y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔\left({y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\wedge {f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)$
77 75 76 syl ${⊢}{f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\to \left({y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔\left({y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\wedge {f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)$
78 77 baibd ${⊢}\left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\right)\to \left({y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
79 78 ralbidva ${⊢}{f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\to \left(\forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔\forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
80 79 ad2antrl ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \left(\forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔\forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)$
81 74 80 mpbird ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]$
82 id ${⊢}{y}={x}\to {y}={x}$
83 oveq1 ${⊢}{y}={x}\to {y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)={x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)$
84 83 imaeq2d ${⊢}{y}={x}\to {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]={{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]$
85 82 84 eleq12d ${⊢}{y}={x}\to \left({y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔{x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)$
86 85 ralrab2 ${⊢}\forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)$
87 81 86 sylib ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)$
88 70 73 87 3jca ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)$
89 88 ex ${⊢}{v}\in \mathrm{Fin}\to \left(\left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\to \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)$
90 49 89 syl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \left(\left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\to \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)$
91 simpr2 ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {f}:\mathrm{dom}{f}⟶{Y}$
92 91 frnd ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \mathrm{ran}{f}\subseteq {Y}$
93 91 ffnd ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {f}Fn\mathrm{dom}{f}$
94 49 adantr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {v}\in \mathrm{Fin}$
95 simpr1 ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \mathrm{dom}{f}\subseteq {v}$
96 ssfi ${⊢}\left({v}\in \mathrm{Fin}\wedge \mathrm{dom}{f}\subseteq {v}\right)\to \mathrm{dom}{f}\in \mathrm{Fin}$
97 94 95 96 syl2anc ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \mathrm{dom}{f}\in \mathrm{Fin}$
98 fnfi ${⊢}\left({f}Fn\mathrm{dom}{f}\wedge \mathrm{dom}{f}\in \mathrm{Fin}\right)\to {f}\in \mathrm{Fin}$
99 93 97 98 syl2anc ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {f}\in \mathrm{Fin}$
100 rnfi ${⊢}{f}\in \mathrm{Fin}\to \mathrm{ran}{f}\in \mathrm{Fin}$
101 99 100 syl ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \mathrm{ran}{f}\in \mathrm{Fin}$
102 elfpw ${⊢}\mathrm{ran}{f}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)↔\left(\mathrm{ran}{f}\subseteq {Y}\wedge \mathrm{ran}{f}\in \mathrm{Fin}\right)$
103 92 101 102 sylanbrc ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \mathrm{ran}{f}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)$
104 oveq1 ${⊢}{x}={z}\to {x}\mathrm{ball}\left({N}\right){c}={z}\mathrm{ball}\left({N}\right){c}$
105 104 cbviunv ${⊢}\bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({N}\right){c}\right)=\bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
106 3 ad4antr ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {z}\in \mathrm{ran}{f}\right)\to {N}\in \mathrm{Met}\left({Y}\right)$
107 metxmet ${⊢}{N}\in \mathrm{Met}\left({Y}\right)\to {N}\in \mathrm{\infty Met}\left({Y}\right)$
108 106 107 syl ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {z}\in \mathrm{ran}{f}\right)\to {N}\in \mathrm{\infty Met}\left({Y}\right)$
109 92 sselda ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {z}\in \mathrm{ran}{f}\right)\to {z}\in {Y}$
110 rpxr ${⊢}{c}\in {ℝ}^{+}\to {c}\in {ℝ}^{*}$
111 110 ad4antlr ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {z}\in \mathrm{ran}{f}\right)\to {c}\in {ℝ}^{*}$
112 blssm ${⊢}\left({N}\in \mathrm{\infty Met}\left({Y}\right)\wedge {z}\in {Y}\wedge {c}\in {ℝ}^{*}\right)\to {z}\mathrm{ball}\left({N}\right){c}\subseteq {Y}$
113 108 109 111 112 syl3anc ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {z}\in \mathrm{ran}{f}\right)\to {z}\mathrm{ball}\left({N}\right){c}\subseteq {Y}$
114 113 ralrimiva ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \forall {z}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}{z}\mathrm{ball}\left({N}\right){c}\subseteq {Y}$
115 iunss ${⊢}\bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)\subseteq {Y}↔\forall {z}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}{z}\mathrm{ball}\left({N}\right){c}\subseteq {Y}$
116 114 115 sylibr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)\subseteq {Y}$
117 iunin1 ${⊢}\bigcup _{{y}\in {v}}\left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\right)=\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}$
118 simplrr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
119 53 cbviunv ${⊢}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)=\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
120 118 119 sseqtrdi ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {Y}\subseteq \bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
121 sseqin2 ${⊢}{Y}\subseteq \bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)↔\bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}={Y}$
122 120 121 sylib ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \bigcup _{{y}\in {v}}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}={Y}$
123 117 122 syl5eq ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \bigcup _{{y}\in {v}}\left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\right)={Y}$
124 0ss ${⊢}\varnothing \subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
125 sseq1 ${⊢}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}=\varnothing \to \left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)↔\varnothing \subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)\right)$
126 124 125 mpbiri ${⊢}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}=\varnothing \to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
127 126 a1i ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {v}\right)\to \left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}=\varnothing \to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)\right)$
128 simpr3 ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)$
129 54 neeq1d ${⊢}{x}={y}\to \left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing ↔\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right)$
130 id ${⊢}{x}={y}\to {x}={y}$
131 53 imaeq2d ${⊢}{x}={y}\to {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]={{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]$
132 130 131 eleq12d ${⊢}{x}={y}\to \left({x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔{y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)$
133 129 132 imbi12d ${⊢}{x}={y}\to \left(\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)↔\left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)$
134 133 rspccva ${⊢}\left(\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\wedge {y}\in {v}\right)\to \left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)$
135 128 134 sylan ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {v}\right)\to \left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)$
136 13 ad5antr ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
137 cnvimass ${⊢}{{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\subseteq \mathrm{dom}{f}$
138 47 simplbi ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {v}\subseteq {X}$
139 138 ad2antrl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to {v}\subseteq {X}$
140 139 adantr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {v}\subseteq {X}$
141 95 140 sstrd ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \mathrm{dom}{f}\subseteq {X}$
142 137 141 sstrid ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\subseteq {X}$
143 142 sselda ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {y}\in {X}$
144 simp-4r ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {c}\in {ℝ}^{+}$
145 144 rpred ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {c}\in ℝ$
146 elpreima ${⊢}{f}Fn\mathrm{dom}{f}\to \left({y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]↔\left({y}\in \mathrm{dom}{f}\wedge {f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)$
147 146 simplbda ${⊢}\left({f}Fn\mathrm{dom}{f}\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
148 93 147 sylan ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)$
149 blhalf ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({c}\in ℝ\wedge {f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to {y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\subseteq {f}\left({y}\right)\mathrm{ball}\left({M}\right){c}$
150 136 143 145 148 149 syl22anc ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\subseteq {f}\left({y}\right)\mathrm{ball}\left({M}\right){c}$
151 150 ssrind ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \left({f}\left({y}\right)\mathrm{ball}\left({M}\right){c}\right)\cap {Y}$
152 137 sseli ${⊢}{y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\to {y}\in \mathrm{dom}{f}$
153 ffvelrn ${⊢}\left({f}:\mathrm{dom}{f}⟶{Y}\wedge {y}\in \mathrm{dom}{f}\right)\to {f}\left({y}\right)\in {Y}$
154 91 152 153 syl2an ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {f}\left({y}\right)\in {Y}$
155 simp-5r ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {Y}\subseteq {X}$
156 155 20 sylib ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {X}\cap {Y}={Y}$
157 154 156 eleqtrrd ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {f}\left({y}\right)\in \left({X}\cap {Y}\right)$
158 110 ad4antlr ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {c}\in {ℝ}^{*}$
159 1 blres ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {f}\left({y}\right)\in \left({X}\cap {Y}\right)\wedge {c}\in {ℝ}^{*}\right)\to {f}\left({y}\right)\mathrm{ball}\left({N}\right){c}=\left({f}\left({y}\right)\mathrm{ball}\left({M}\right){c}\right)\cap {Y}$
160 136 157 158 159 syl3anc ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {f}\left({y}\right)\mathrm{ball}\left({N}\right){c}=\left({f}\left({y}\right)\mathrm{ball}\left({M}\right){c}\right)\cap {Y}$
161 151 160 sseqtrrd ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq {f}\left({y}\right)\mathrm{ball}\left({N}\right){c}$
162 fnfvelrn ${⊢}\left({f}Fn\mathrm{dom}{f}\wedge {y}\in \mathrm{dom}{f}\right)\to {f}\left({y}\right)\in \mathrm{ran}{f}$
163 93 152 162 syl2an ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {f}\left({y}\right)\in \mathrm{ran}{f}$
164 oveq1 ${⊢}{z}={f}\left({y}\right)\to {z}\mathrm{ball}\left({N}\right){c}={f}\left({y}\right)\mathrm{ball}\left({N}\right){c}$
165 164 ssiun2s ${⊢}{f}\left({y}\right)\in \mathrm{ran}{f}\to {f}\left({y}\right)\mathrm{ball}\left({N}\right){c}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
166 163 165 syl ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to {f}\left({y}\right)\mathrm{ball}\left({N}\right){c}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
167 161 166 sstrd ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
168 167 adantlr ${⊢}\left(\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {v}\right)\wedge {y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
169 168 ex ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {v}\right)\to \left({y}\in {{f}}^{-1}\left[{y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)\right)$
170 135 169 syld ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {v}\right)\to \left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)\right)$
171 127 170 pm2.61dne ${⊢}\left(\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\wedge {y}\in {v}\right)\to \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
172 171 ralrimiva ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \forall {y}\in {v}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
173 iunss ${⊢}\bigcup _{{y}\in {v}}\left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\right)\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)↔\forall {y}\in {v}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
174 172 173 sylibr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \bigcup _{{y}\in {v}}\left(\left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\right)\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
175 123 174 eqsstrrd ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to {Y}\subseteq \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)$
176 116 175 eqssd ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \bigcup _{{z}\in \mathrm{ran}{f}}\left({z}\mathrm{ball}\left({N}\right){c}\right)={Y}$
177 105 176 syl5eq ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}$
178 iuneq1 ${⊢}{w}=\mathrm{ran}{f}\to \bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)=\bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({N}\right){c}\right)$
179 178 eqeq1d ${⊢}{w}=\mathrm{ran}{f}\to \left(\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}↔\bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
180 179 rspcev ${⊢}\left(\mathrm{ran}{f}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)\to \exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}$
181 103 177 180 syl2anc ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\wedge \left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\right)\to \exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}$
182 181 ex ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \left(\left(\mathrm{dom}{f}\subseteq {v}\wedge {f}:\mathrm{dom}{f}⟶{Y}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \to {x}\in {{f}}^{-1}\left[{x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right]\right)\right)\to \exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
183 90 182 syld ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \left(\left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\to \exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
184 183 exlimdv ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}⟶{Y}\wedge \forall {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({y}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\to \exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
185 67 184 mpd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\right)\right)\to \exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}$
186 185 rexlimdvaa ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)\left(\frac{{c}}{2}\right)\right)\to \exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
187 46 186 syld ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {c}\in {ℝ}^{+}\right)\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
188 187 ralrimdva ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\to \forall {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
189 istotbnd3 ${⊢}{N}\in \mathrm{TotBnd}\left({Y}\right)↔\left({N}\in \mathrm{Met}\left({Y}\right)\wedge \forall {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
190 189 baib ${⊢}{N}\in \mathrm{Met}\left({Y}\right)\to \left({N}\in \mathrm{TotBnd}\left({Y}\right)↔\forall {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
191 3 190 syl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({N}\in \mathrm{TotBnd}\left({Y}\right)↔\forall {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(𝒫{Y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {w}}\left({x}\mathrm{ball}\left({N}\right){c}\right)={Y}\right)$
192 188 191 sylibrd ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\to {N}\in \mathrm{TotBnd}\left({Y}\right)\right)$
193 38 192 impbid ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({N}\in \mathrm{TotBnd}\left({Y}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$