# Metamath Proof Explorer

## Theorem istotbnd3

Description: A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion istotbnd3 ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$

### Proof

Step Hyp Ref Expression
1 istotbnd ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
2 oveq1 ${⊢}{x}={f}\left({b}\right)\to {x}\mathrm{ball}\left({M}\right){d}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}$
3 2 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)$
4 3 ac6sfi ${⊢}\left({w}\in \mathrm{Fin}\wedge \forall {b}\in {w}\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}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
5 4 ex ${⊢}{w}\in \mathrm{Fin}\to \left(\forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
6 5 ad2antlr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \bigcup {w}={X}\right)\to \left(\forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
7 simprrl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to {f}:{w}⟶{X}$
8 7 frnd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \mathrm{ran}{f}\subseteq {X}$
9 simplr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to {w}\in \mathrm{Fin}$
10 7 ffnd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to {f}Fn{w}$
11 dffn4 ${⊢}{f}Fn{w}↔{f}:{w}\underset{onto}{⟶}\mathrm{ran}{f}$
12 10 11 sylib ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to {f}:{w}\underset{onto}{⟶}\mathrm{ran}{f}$
13 fofi ${⊢}\left({w}\in \mathrm{Fin}\wedge {f}:{w}\underset{onto}{⟶}\mathrm{ran}{f}\right)\to \mathrm{ran}{f}\in \mathrm{Fin}$
14 9 12 13 syl2anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \mathrm{ran}{f}\in \mathrm{Fin}$
15 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)$
16 8 14 15 sylanbrc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \mathrm{ran}{f}\in \left(𝒫{X}\cap \mathrm{Fin}\right)$
17 2 eleq2d ${⊢}{x}={f}\left({b}\right)\to \left({v}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)↔{v}\in \left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
18 17 rexrn ${⊢}{f}Fn{w}\to \left(\exists {x}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}{v}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)↔\exists {b}\in {w}\phantom{\rule{.4em}{0ex}}{v}\in \left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
19 10 18 syl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \left(\exists {x}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}{v}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)↔\exists {b}\in {w}\phantom{\rule{.4em}{0ex}}{v}\in \left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
20 eliun ${⊢}{v}\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}}{v}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)$
21 eliun ${⊢}{v}\in \bigcup _{{b}\in {w}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)↔\exists {b}\in {w}\phantom{\rule{.4em}{0ex}}{v}\in \left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
22 19 20 21 3bitr4g ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \left({v}\in \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔{v}\in \bigcup _{{b}\in {w}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)$
23 22 eqrdv ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup _{{b}\in {w}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
24 simprrr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}$
25 iuneq2 ${⊢}\forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\to \bigcup _{{b}\in {w}}{b}=\bigcup _{{b}\in {w}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
26 24 25 syl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \bigcup _{{b}\in {w}}{b}=\bigcup _{{b}\in {w}}\left({f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)$
27 uniiun ${⊢}\bigcup {w}=\bigcup _{{b}\in {w}}{b}$
28 simprl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \bigcup {w}={X}$
29 27 28 syl5eqr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \bigcup _{{b}\in {w}}{b}={X}$
30 23 26 29 3eqtr2d ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}$
31 iuneq1 ${⊢}{v}=\mathrm{ran}{f}\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
32 31 eqeq1d ${⊢}{v}=\mathrm{ran}{f}\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}↔\bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
33 32 rspcev ${⊢}\left(\mathrm{ran}{f}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in \mathrm{ran}{f}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}$
34 16 30 33 syl2anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \left(\bigcup {w}={X}\wedge \left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\right)\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}$
35 34 expr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \bigcup {w}={X}\right)\to \left(\left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
36 35 exlimdv ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \bigcup {w}={X}\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{w}⟶{X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}{b}={f}\left({b}\right)\mathrm{ball}\left({M}\right){d}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
37 6 36 syld ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\wedge \bigcup {w}={X}\right)\to \left(\forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
38 37 expimpd ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {w}\in \mathrm{Fin}\right)\to \left(\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
39 38 rexlimdva ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
40 elfpw ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)↔\left({v}\subseteq {X}\wedge {v}\in \mathrm{Fin}\right)$
41 40 simprbi ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {v}\in \mathrm{Fin}$
42 41 ad2antrl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to {v}\in \mathrm{Fin}$
43 mptfi ${⊢}{v}\in \mathrm{Fin}\to \left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}$
44 rnfi ${⊢}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}\to \mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}$
45 42 43 44 3syl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to \mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}$
46 ovex ${⊢}{x}\mathrm{ball}\left({M}\right){d}\in \mathrm{V}$
47 46 dfiun3 ${⊢}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup \mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)$
48 simprr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}$
49 47 48 syl5eqr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to \bigcup \mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)={X}$
50 eqid ${⊢}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)=\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)$
51 50 rnmpt ${⊢}\mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)=\left\{{b}|\exists {x}\in {v}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}$
52 40 simplbi ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {v}\subseteq {X}$
53 52 ad2antrl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to {v}\subseteq {X}$
54 ssrexv ${⊢}{v}\subseteq {X}\to \left(\exists {x}\in {v}\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)$
55 53 54 syl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to \left(\exists {x}\in {v}\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)$
56 55 ss2abdv ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to \left\{{b}|\exists {x}\in {v}\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\}$
57 51 56 eqsstrid ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to \mathrm{ran}\left({x}\in {v}⟼{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\}$
58 unieq ${⊢}{w}=\mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \bigcup {w}=\bigcup \mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)$
59 58 eqeq1d ${⊢}{w}=\mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \left(\bigcup {w}={X}↔\bigcup \mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
60 ssabral ${⊢}{w}\subseteq \left\{{b}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right\}↔\forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}$
61 sseq1 ${⊢}{w}=\mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \left({w}\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 {v}⟼{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)$
62 60 61 bitr3id ${⊢}{w}=\mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \left(\forall {b}\in {w}\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 {v}⟼{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)$
63 59 62 anbi12d ${⊢}{w}=\mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\to \left(\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)↔\left(\bigcup \mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)={X}\wedge \mathrm{ran}\left({x}\in {v}⟼{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)$
64 63 rspcev ${⊢}\left(\mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)\in \mathrm{Fin}\wedge \left(\bigcup \mathrm{ran}\left({x}\in {v}⟼{x}\mathrm{ball}\left({M}\right){d}\right)={X}\wedge \mathrm{ran}\left({x}\in {v}⟼{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 {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
65 45 49 57 64 syl12anc ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)\right)\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
66 65 expr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
67 66 rexlimdva ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
68 39 67 impbid ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)↔\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
69 68 ralbidv ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
70 69 pm5.32i ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {w}={X}\wedge \forall {b}\in {w}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
71 1 70 bitri ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$