# Metamath Proof Explorer

## Theorem sstotbnd3

Description: Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 ${⊢}{N}={{M}↾}_{\left({Y}×{Y}\right)}$
Assertion sstotbnd3 ${⊢}\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 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\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 {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)$
3 elin ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)↔\left({v}\in 𝒫{X}\wedge {v}\in \mathrm{Fin}\right)$
4 rabfi ${⊢}{v}\in \mathrm{Fin}\to \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}$
5 4 anim2i ${⊢}\left({v}\in 𝒫{X}\wedge {v}\in \mathrm{Fin}\right)\to \left({v}\in 𝒫{X}\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
6 3 5 sylbi ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to \left({v}\in 𝒫{X}\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
7 6 anim2i ${⊢}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\right)\to \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left({v}\in 𝒫{X}\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)$
8 7 ancoms ${⊢}\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)\to \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left({v}\in 𝒫{X}\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)$
9 an12 ${⊢}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left({v}\in 𝒫{X}\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)↔\left({v}\in 𝒫{X}\wedge \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)$
10 8 9 sylib ${⊢}\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)\to \left({v}\in 𝒫{X}\wedge \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)$
11 10 reximi2 ${⊢}\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 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
12 11 ralimi ${⊢}\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 {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
13 2 12 syl6bi ${⊢}\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 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)$
14 ssrab2 ${⊢}\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\subseteq {v}$
15 elpwi ${⊢}{v}\in 𝒫{X}\to {v}\subseteq {X}$
16 15 ad2antlr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {v}\in 𝒫{X}\right)\wedge \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)\to {v}\subseteq {X}$
17 14 16 sstrid ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {v}\in 𝒫{X}\right)\wedge \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)\to \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\subseteq {X}$
18 simprr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {v}\in 𝒫{X}\right)\wedge \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)\to \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}$
19 elfpw ${⊢}\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \left(𝒫{X}\cap \mathrm{Fin}\right)↔\left(\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\subseteq {X}\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
20 17 18 19 sylanbrc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {v}\in 𝒫{X}\right)\wedge \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)\to \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \left(𝒫{X}\cap \mathrm{Fin}\right)$
21 ssel2 ${⊢}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge {z}\in {Y}\right)\to {z}\in \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)$
22 eliun ${⊢}{z}\in \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)↔\exists {x}\in {v}\phantom{\rule{.4em}{0ex}}{z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)$
23 21 22 sylib ${⊢}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge {z}\in {Y}\right)\to \exists {x}\in {v}\phantom{\rule{.4em}{0ex}}{z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)$
24 inelcm ${⊢}\left({z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge {z}\in {Y}\right)\to \left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing$
25 24 expcom ${⊢}{z}\in {Y}\to \left({z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\to \left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right)$
26 25 ancrd ${⊢}{z}\in {Y}\to \left({z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\to \left(\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \wedge {z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)$
27 26 reximdv ${⊢}{z}\in {Y}\to \left(\exists {x}\in {v}\phantom{\rule{.4em}{0ex}}{z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \wedge {z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\right)\right)$
28 27 impcom ${⊢}\left(\exists {x}\in {v}\phantom{\rule{.4em}{0ex}}{z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge {z}\in {Y}\right)\to \exists {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \wedge {z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
29 23 28 sylancom ${⊢}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge {z}\in {Y}\right)\to \exists {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \wedge {z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
30 eliun ${⊢}{z}\in \bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)↔\exists {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{z}\in \left({y}\mathrm{ball}\left({M}\right){d}\right)$
31 oveq1 ${⊢}{y}={x}\to {y}\mathrm{ball}\left({M}\right){d}={x}\mathrm{ball}\left({M}\right){d}$
32 31 eleq2d ${⊢}{y}={x}\to \left({z}\in \left({y}\mathrm{ball}\left({M}\right){d}\right)↔{z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
33 32 rexrab2 ${⊢}\exists {y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\phantom{\rule{.4em}{0ex}}{z}\in \left({y}\mathrm{ball}\left({M}\right){d}\right)↔\exists {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \wedge {z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
34 30 33 bitri ${⊢}{z}\in \bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)↔\exists {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \wedge {z}\in \left({x}\mathrm{ball}\left({M}\right){d}\right)\right)$
35 29 34 sylibr ${⊢}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge {z}\in {Y}\right)\to {z}\in \bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)$
36 35 ex ${⊢}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\to \left({z}\in {Y}\to {z}\in \bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)\right)$
37 36 ssrdv ${⊢}{Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\to {Y}\subseteq \bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)$
38 37 ad2antrl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {v}\in 𝒫{X}\right)\wedge \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)\to {Y}\subseteq \bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)$
39 iuneq1 ${⊢}{w}=\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\to \bigcup _{{y}\in {w}}\left({y}\mathrm{ball}\left({M}\right){d}\right)=\bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)$
40 39 sseq2d ${⊢}{w}=\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\to \left({Y}\subseteq \bigcup _{{y}\in {w}}\left({y}\mathrm{ball}\left({M}\right){d}\right)↔{Y}\subseteq \bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)\right)$
41 40 rspcev ${⊢}\left(\left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge {Y}\subseteq \bigcup _{{y}\in \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}}\left({y}\mathrm{ball}\left({M}\right){d}\right)\right)\to \exists {w}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{y}\in {w}}\left({y}\mathrm{ball}\left({M}\right){d}\right)$
42 20 38 41 syl2anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {v}\in 𝒫{X}\right)\wedge \left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)\to \exists {w}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{y}\in {w}}\left({y}\mathrm{ball}\left({M}\right){d}\right)$
43 42 rexlimdva2 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\exists {v}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\to \exists {w}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{y}\in {w}}\left({y}\mathrm{ball}\left({M}\right){d}\right)\right)$
44 43 ralimdv ${⊢}\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 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{y}\in {w}}\left({y}\mathrm{ball}\left({M}\right){d}\right)\right)$
45 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 {w}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{Y}\subseteq \bigcup _{{y}\in {w}}\left({y}\mathrm{ball}\left({M}\right){d}\right)\right)$
46 44 45 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 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\to {N}\in \mathrm{TotBnd}\left({Y}\right)\right)$
47 13 46 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 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({Y}\subseteq \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)\wedge \left\{{x}\in {v}|\left({x}\mathrm{ball}\left({M}\right){d}\right)\cap {Y}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)$