Metamath Proof Explorer

Theorem xblss2ps

Description: One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 for extended metrics, we have to assume the balls are a finite distance apart, or else P will not even be in the infinity ball around Q . (Contributed by Mario Carneiro, 23-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Hypotheses xblss2ps.1 ${⊢}{\phi }\to {D}\in \mathrm{PsMet}\left({X}\right)$
xblss2ps.2 ${⊢}{\phi }\to {P}\in {X}$
xblss2ps.3 ${⊢}{\phi }\to {Q}\in {X}$
xblss2ps.4 ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
xblss2ps.5 ${⊢}{\phi }\to {S}\in {ℝ}^{*}$
xblss2ps.6 ${⊢}{\phi }\to {P}{D}{Q}\in ℝ$
xblss2ps.7 ${⊢}{\phi }\to {P}{D}{Q}\le {S}{+}_{𝑒}\left(-{R}\right)$
Assertion xblss2ps ${⊢}{\phi }\to {P}\mathrm{ball}\left({D}\right){R}\subseteq {Q}\mathrm{ball}\left({D}\right){S}$

Proof

Step Hyp Ref Expression
1 xblss2ps.1 ${⊢}{\phi }\to {D}\in \mathrm{PsMet}\left({X}\right)$
2 xblss2ps.2 ${⊢}{\phi }\to {P}\in {X}$
3 xblss2ps.3 ${⊢}{\phi }\to {Q}\in {X}$
4 xblss2ps.4 ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
5 xblss2ps.5 ${⊢}{\phi }\to {S}\in {ℝ}^{*}$
6 xblss2ps.6 ${⊢}{\phi }\to {P}{D}{Q}\in ℝ$
7 xblss2ps.7 ${⊢}{\phi }\to {P}{D}{Q}\le {S}{+}_{𝑒}\left(-{R}\right)$
8 elblps ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to \left({x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)↔\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\right)$
9 1 2 4 8 syl3anc ${⊢}{\phi }\to \left({x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)↔\left({x}\in {X}\wedge {P}{D}{x}<{R}\right)\right)$
10 9 simprbda ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {x}\in {X}$
11 1 adantr ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {D}\in \mathrm{PsMet}\left({X}\right)$
12 3 adantr ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {Q}\in {X}$
13 psmetcl ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {Q}\in {X}\wedge {x}\in {X}\right)\to {Q}{D}{x}\in {ℝ}^{*}$
14 11 12 10 13 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {Q}{D}{x}\in {ℝ}^{*}$
15 14 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}\in ℝ\right)\to {Q}{D}{x}\in {ℝ}^{*}$
16 6 adantr ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}{D}{Q}\in ℝ$
17 16 rexrd ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}{D}{Q}\in {ℝ}^{*}$
18 4 adantr ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {R}\in {ℝ}^{*}$
19 17 18 xaddcld ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to \left({P}{D}{Q}\right){+}_{𝑒}{R}\in {ℝ}^{*}$
20 19 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}\in ℝ\right)\to \left({P}{D}{Q}\right){+}_{𝑒}{R}\in {ℝ}^{*}$
21 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}\in ℝ\right)\to {S}\in {ℝ}^{*}$
22 2 adantr ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}\in {X}$
23 psmetcl ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {x}\in {X}\right)\to {P}{D}{x}\in {ℝ}^{*}$
24 11 22 10 23 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}{D}{x}\in {ℝ}^{*}$
25 17 24 xaddcld ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to \left({P}{D}{Q}\right){+}_{𝑒}\left({P}{D}{x}\right)\in {ℝ}^{*}$
26 psmettri2 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge \left({P}\in {X}\wedge {Q}\in {X}\wedge {x}\in {X}\right)\right)\to {Q}{D}{x}\le \left({P}{D}{Q}\right){+}_{𝑒}\left({P}{D}{x}\right)$
27 11 22 12 10 26 syl13anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {Q}{D}{x}\le \left({P}{D}{Q}\right){+}_{𝑒}\left({P}{D}{x}\right)$
28 9 simplbda ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}{D}{x}<{R}$
29 xltadd2 ${⊢}\left({P}{D}{x}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\wedge {P}{D}{Q}\in ℝ\right)\to \left({P}{D}{x}<{R}↔\left({P}{D}{Q}\right){+}_{𝑒}\left({P}{D}{x}\right)<\left({P}{D}{Q}\right){+}_{𝑒}{R}\right)$
30 24 18 16 29 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to \left({P}{D}{x}<{R}↔\left({P}{D}{Q}\right){+}_{𝑒}\left({P}{D}{x}\right)<\left({P}{D}{Q}\right){+}_{𝑒}{R}\right)$
31 28 30 mpbid ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to \left({P}{D}{Q}\right){+}_{𝑒}\left({P}{D}{x}\right)<\left({P}{D}{Q}\right){+}_{𝑒}{R}$
32 14 25 19 27 31 xrlelttrd ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {Q}{D}{x}<\left({P}{D}{Q}\right){+}_{𝑒}{R}$
33 32 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}\in ℝ\right)\to {Q}{D}{x}<\left({P}{D}{Q}\right){+}_{𝑒}{R}$
34 5 adantr ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {S}\in {ℝ}^{*}$
35 18 xnegcld ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to -{R}\in {ℝ}^{*}$
36 34 35 xaddcld ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {S}{+}_{𝑒}\left(-{R}\right)\in {ℝ}^{*}$
37 7 adantr ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}{D}{Q}\le {S}{+}_{𝑒}\left(-{R}\right)$
38 xleadd1a ${⊢}\left(\left({P}{D}{Q}\in {ℝ}^{*}\wedge {S}{+}_{𝑒}\left(-{R}\right)\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\right)\wedge {P}{D}{Q}\le {S}{+}_{𝑒}\left(-{R}\right)\right)\to \left({P}{D}{Q}\right){+}_{𝑒}{R}\le \left({S}{+}_{𝑒}\left(-{R}\right)\right){+}_{𝑒}{R}$
39 17 36 18 37 38 syl31anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to \left({P}{D}{Q}\right){+}_{𝑒}{R}\le \left({S}{+}_{𝑒}\left(-{R}\right)\right){+}_{𝑒}{R}$
40 39 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}\in ℝ\right)\to \left({P}{D}{Q}\right){+}_{𝑒}{R}\le \left({S}{+}_{𝑒}\left(-{R}\right)\right){+}_{𝑒}{R}$
41 xnpcan ${⊢}\left({S}\in {ℝ}^{*}\wedge {R}\in ℝ\right)\to \left({S}{+}_{𝑒}\left(-{R}\right)\right){+}_{𝑒}{R}={S}$
42 34 41 sylan ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}\in ℝ\right)\to \left({S}{+}_{𝑒}\left(-{R}\right)\right){+}_{𝑒}{R}={S}$
43 40 42 breqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}\in ℝ\right)\to \left({P}{D}{Q}\right){+}_{𝑒}{R}\le {S}$
44 15 20 21 33 43 xrltletrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}\in ℝ\right)\to {Q}{D}{x}<{S}$
45 14 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {Q}{D}{x}\in {ℝ}^{*}$
46 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {P}{D}{Q}\in ℝ$
47 simpll ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {\phi }$
48 simplr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)$
49 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {R}=\mathrm{+\infty }$
50 49 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {P}\mathrm{ball}\left({D}\right){R}={P}\mathrm{ball}\left({D}\right)\mathrm{+\infty }$
51 48 50 eleqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {x}\in \left({P}\mathrm{ball}\left({D}\right)\mathrm{+\infty }\right)$
52 xblpnfps ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\right)\to \left({x}\in \left({P}\mathrm{ball}\left({D}\right)\mathrm{+\infty }\right)↔\left({x}\in {X}\wedge {P}{D}{x}\in ℝ\right)\right)$
53 1 2 52 syl2anc ${⊢}{\phi }\to \left({x}\in \left({P}\mathrm{ball}\left({D}\right)\mathrm{+\infty }\right)↔\left({x}\in {X}\wedge {P}{D}{x}\in ℝ\right)\right)$
54 53 simplbda ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right)\mathrm{+\infty }\right)\right)\to {P}{D}{x}\in ℝ$
55 47 51 54 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {P}{D}{x}\in ℝ$
56 46 55 readdcld ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \left({P}{D}{Q}\right)+\left({P}{D}{x}\right)\in ℝ$
57 56 rexrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \left({P}{D}{Q}\right)+\left({P}{D}{x}\right)\in {ℝ}^{*}$
58 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
59 58 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
60 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {D}\in \mathrm{PsMet}\left({X}\right)$
61 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {P}\in {X}$
62 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {Q}\in {X}$
63 10 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {x}\in {X}$
64 60 61 62 63 26 syl13anc ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {Q}{D}{x}\le \left({P}{D}{Q}\right){+}_{𝑒}\left({P}{D}{x}\right)$
65 46 55 rexaddd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \left({P}{D}{Q}\right){+}_{𝑒}\left({P}{D}{x}\right)=\left({P}{D}{Q}\right)+\left({P}{D}{x}\right)$
66 64 65 breqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {Q}{D}{x}\le \left({P}{D}{Q}\right)+\left({P}{D}{x}\right)$
67 56 ltpnfd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \left({P}{D}{Q}\right)+\left({P}{D}{x}\right)<\mathrm{+\infty }$
68 45 57 59 66 67 xrlelttrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {Q}{D}{x}<\mathrm{+\infty }$
69 0xr ${⊢}0\in {ℝ}^{*}$
70 69 a1i ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0\in {ℝ}^{*}$
71 psmetge0 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to 0\le {P}{D}{Q}$
72 11 22 12 71 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0\le {P}{D}{Q}$
73 70 17 36 72 37 xrletrd ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0\le {S}{+}_{𝑒}\left(-{R}\right)$
74 ge0nemnf ${⊢}\left({S}{+}_{𝑒}\left(-{R}\right)\in {ℝ}^{*}\wedge 0\le {S}{+}_{𝑒}\left(-{R}\right)\right)\to {S}{+}_{𝑒}\left(-{R}\right)\ne \mathrm{-\infty }$
75 36 73 74 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {S}{+}_{𝑒}\left(-{R}\right)\ne \mathrm{-\infty }$
76 75 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {S}{+}_{𝑒}\left(-{R}\right)\ne \mathrm{-\infty }$
77 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {S}\in {ℝ}^{*}$
78 xaddmnf1 ${⊢}\left({S}\in {ℝ}^{*}\wedge {S}\ne \mathrm{+\infty }\right)\to {S}{+}_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }$
79 78 ex ${⊢}{S}\in {ℝ}^{*}\to \left({S}\ne \mathrm{+\infty }\to {S}{+}_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }\right)$
80 77 79 syl ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \left({S}\ne \mathrm{+\infty }\to {S}{+}_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }\right)$
81 xnegeq ${⊢}{R}=\mathrm{+\infty }\to -{R}=-\mathrm{+\infty }$
82 49 81 syl ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to -{R}=-\mathrm{+\infty }$
83 xnegpnf ${⊢}-\mathrm{+\infty }=\mathrm{-\infty }$
84 82 83 syl6eq ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to -{R}=\mathrm{-\infty }$
85 84 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {S}{+}_{𝑒}\left(-{R}\right)={S}{+}_{𝑒}\mathrm{-\infty }$
86 85 eqeq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \left({S}{+}_{𝑒}\left(-{R}\right)=\mathrm{-\infty }↔{S}{+}_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }\right)$
87 80 86 sylibrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \left({S}\ne \mathrm{+\infty }\to {S}{+}_{𝑒}\left(-{R}\right)=\mathrm{-\infty }\right)$
88 87 necon1d ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to \left({S}{+}_{𝑒}\left(-{R}\right)\ne \mathrm{-\infty }\to {S}=\mathrm{+\infty }\right)$
89 76 88 mpd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {S}=\mathrm{+\infty }$
90 68 89 breqtrrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\wedge {R}=\mathrm{+\infty }\right)\to {Q}{D}{x}<{S}$
91 psmetge0 ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {P}\in {X}\wedge {x}\in {X}\right)\to 0\le {P}{D}{x}$
92 11 22 10 91 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0\le {P}{D}{x}$
93 70 24 18 92 28 xrlelttrd ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0<{R}$
94 70 18 93 xrltled ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0\le {R}$
95 ge0nemnf ${⊢}\left({R}\in {ℝ}^{*}\wedge 0\le {R}\right)\to {R}\ne \mathrm{-\infty }$
96 18 94 95 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {R}\ne \mathrm{-\infty }$
97 18 96 jca ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to \left({R}\in {ℝ}^{*}\wedge {R}\ne \mathrm{-\infty }\right)$
98 xrnemnf ${⊢}\left({R}\in {ℝ}^{*}\wedge {R}\ne \mathrm{-\infty }\right)↔\left({R}\in ℝ\vee {R}=\mathrm{+\infty }\right)$
99 97 98 sylib ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to \left({R}\in ℝ\vee {R}=\mathrm{+\infty }\right)$
100 44 90 99 mpjaodan ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {Q}{D}{x}<{S}$
101 elblps ${⊢}\left({D}\in \mathrm{PsMet}\left({X}\right)\wedge {Q}\in {X}\wedge {S}\in {ℝ}^{*}\right)\to \left({x}\in \left({Q}\mathrm{ball}\left({D}\right){S}\right)↔\left({x}\in {X}\wedge {Q}{D}{x}<{S}\right)\right)$
102 11 12 34 101 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to \left({x}\in \left({Q}\mathrm{ball}\left({D}\right){S}\right)↔\left({x}\in {X}\wedge {Q}{D}{x}<{S}\right)\right)$
103 10 100 102 mpbir2and ${⊢}\left({\phi }\wedge {x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {x}\in \left({Q}\mathrm{ball}\left({D}\right){S}\right)$
104 103 ex ${⊢}{\phi }\to \left({x}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\to {x}\in \left({Q}\mathrm{ball}\left({D}\right){S}\right)\right)$
105 104 ssrdv ${⊢}{\phi }\to {P}\mathrm{ball}\left({D}\right){R}\subseteq {Q}\mathrm{ball}\left({D}\right){S}$