# Metamath Proof Explorer

## Theorem sstotbnd

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

Ref Expression
Hypothesis sstotbnd.2 ${⊢}{N}={{M}↾}_{\left({Y}×{Y}\right)}$
Assertion sstotbnd ${⊢}\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 \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$

### Proof

Step Hyp Ref Expression
1 sstotbnd.2 ${⊢}{N}={{M}↾}_{\left({Y}×{Y}\right)}$
2 1 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 {u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
3 elfpw ${⊢}{u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)↔\left({u}\subseteq {X}\wedge {u}\in \mathrm{Fin}\right)$
4 3 simprbi ${⊢}{u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {u}\in \mathrm{Fin}$
5 mptfi ${⊢}{u}\in \mathrm{Fin}\to \left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}$
6 rnfi ${⊢}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}\to \mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}$
7 4 5 6 3syl ${⊢}{u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to \mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}$
8 7 ad2antrl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}$
9 simprr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to {Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
10 eqid ${⊢}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)=\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)$
11 10 rnmpt ${⊢}\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)=\left\{{b}|\exists {x}\in {u}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}$
12 3 simplbi ${⊢}{u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {u}\subseteq {X}$
13 ssrexv ${⊢}{u}\subseteq {X}\to \left(\exists {x}\in {u}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
14 12 13 syl ${⊢}{u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to \left(\exists {x}\in {u}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
15 14 ad2antrl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \left(\exists {x}\in {u}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
16 15 ss2abdv ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \left\{{b}|\exists {x}\in {u}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}$
17 11 16 eqsstrid ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}$
18 unieq ${⊢}{v}=\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \bigcup {v}=\bigcup \mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)$
19 ovex ${⊢}{x}\mathrm{ball}\left({M}\right){d}\in \mathrm{V}$
20 19 dfiun3 ${⊢}\bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup \mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)$
21 18 20 syl6eqr ${⊢}{v}=\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \bigcup {v}=\bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
22 21 sseq2d ${⊢}{v}=\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \left({Y}\subseteq \bigcup {v}↔{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
23 ssabral ${⊢}{v}\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}↔\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}$
24 sseq1 ${⊢}{v}=\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \left({v}\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}↔\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}\right)$
25 23 24 bitr3id ${⊢}{v}=\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \left(\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}↔\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}\right)$
26 22 25 anbi12d ${⊢}{v}=\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \left(\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)↔\left({Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}\right)\right)$
27 26 rspcev ${⊢}\left(\mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \mathrm{ran}\left({x}\in {u}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}\right)\right)\to \exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
28 8 9 17 27 syl12anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
29 28 rexlimdvaa ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\exists {u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
30 oveq1 ${⊢}{x}={f}\left({b}\right)\to {x}\mathrm{ball}\left({M}\right){d}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}$
31 30 eqeq2d ${⊢}{x}={f}\left({b}\right)\to \left({b}={x}\mathrm{ball}\left({M}\right){d}↔{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
32 31 ac6sfi ${⊢}\left({v}\in \mathrm{Fin}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
33 32 adantrl ${⊢}\left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
34 33 adantl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
35 frn ${⊢}{f}:{v}⟶{X}\to \mathrm{ran}{f}\subseteq {X}$
36 35 ad2antrl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to \mathrm{ran}{f}\subseteq {X}$
37 simplrl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to {v}\in \mathrm{Fin}$
38 ffn ${⊢}{f}:{v}⟶{X}\to {f}Fn{v}$
39 38 ad2antrl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to {f}Fn{v}$
40 dffn4 ${⊢}{f}Fn{v}↔{f}:{v}\underset{onto}{⟶}\mathrm{ran}{f}$
41 39 40 sylib ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to {f}:{v}\underset{onto}{⟶}\mathrm{ran}{f}$
42 fofi ${⊢}\left({v}\in \mathrm{Fin}\wedge {f}:{v}\underset{onto}{⟶}\mathrm{ran}{f}\right)\to \mathrm{ran}{f}\in \mathrm{Fin}$
43 37 41 42 syl2anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to \mathrm{ran}{f}\in \mathrm{Fin}$
44 elfpw ${⊢}\mathrm{ran}{f}\in \left(𝒫{X}\cap \mathrm{Fin}\right)↔\left(\mathrm{ran}{f}\subseteq {X}\wedge \mathrm{ran}{f}\in \mathrm{Fin}\right)$
45 36 43 44 sylanbrc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to \mathrm{ran}{f}\in \left(𝒫{X}\cap \mathrm{Fin}\right)$
46 simprrl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to {Y}\subseteq \bigcup {v}$
47 46 adantr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to {Y}\subseteq \bigcup {v}$
48 uniiun ${⊢}\bigcup {v}=\bigcup _{{b}\in {v}}{b}$
49 iuneq2 ${⊢}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\to \bigcup _{{b}\in {v}}{b}=\bigcup _{{b}\in {v}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
50 48 49 syl5eq ${⊢}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\to \bigcup {v}=\bigcup _{{b}\in {v}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
51 50 ad2antll ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to \bigcup {v}=\bigcup _{{b}\in {v}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
52 47 51 sseqtrd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to {Y}\subseteq \bigcup _{{b}\in {v}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
53 30 eleq2d ${⊢}{x}={f}\left({b}\right)\to \left({y}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)↔{y}\in \left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
54 53 rexrn ${⊢}{f}Fn{v}\to \left(\exists {x}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}{y}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)↔\exists {b}\in {v}\phantom{\rule{.4em}{0ex}}{y}\in \left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
55 eliun ${⊢}{y}\in \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔\exists {x}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}{y}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)$
56 eliun ${⊢}{y}\in \bigcup _{{b}\in {v}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)↔\exists {b}\in {v}\phantom{\rule{.4em}{0ex}}{y}\in \left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
57 54 55 56 3bitr4g ${⊢}{f}Fn{v}\to \left({y}\in \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔{y}\in \bigcup _{{b}\in {v}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
58 57 eqrdv ${⊢}{f}Fn{v}\to \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup _{{b}\in {v}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
59 39 58 syl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup _{{b}\in {v}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
60 52 59 sseqtrrd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to {Y}\subseteq \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
61 iuneq1 ${⊢}{u}=\mathrm{ran}{f}\to \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
62 61 sseq2d ${⊢}{u}=\mathrm{ran}{f}\to \left({Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔{Y}\subseteq \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
63 62 rspcev ${⊢}\left(\mathrm{ran}{f}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\to \exists {u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
64 45 60 63 syl2anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\wedge \left({f}:{v}⟶{X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\to \exists {u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
65 34 64 exlimddv ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({v}\in \mathrm{Fin}\wedge \left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \exists {u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
66 65 rexlimdvaa ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
67 29 66 impbid ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\exists {u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
68 67 ralbidv ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{x}\in {u}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
69 2 68 bitrd ${⊢}\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 \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$