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 ( 𝜑𝐷 ∈ ( PsMet ‘ 𝑋 ) )
xblss2ps.2 ( 𝜑𝑃𝑋 )
xblss2ps.3 ( 𝜑𝑄𝑋 )
xblss2ps.4 ( 𝜑𝑅 ∈ ℝ* )
xblss2ps.5 ( 𝜑𝑆 ∈ ℝ* )
xblss2ps.6 ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
xblss2ps.7 ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
Assertion xblss2ps ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )

Proof

Step Hyp Ref Expression
1 xblss2ps.1 ( 𝜑𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2 xblss2ps.2 ( 𝜑𝑃𝑋 )
3 xblss2ps.3 ( 𝜑𝑄𝑋 )
4 xblss2ps.4 ( 𝜑𝑅 ∈ ℝ* )
5 xblss2ps.5 ( 𝜑𝑆 ∈ ℝ* )
6 xblss2ps.6 ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
7 xblss2ps.7 ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
8 elblps ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
9 1 2 4 8 syl3anc ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
10 9 simprbda ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥𝑋 )
11 1 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
12 3 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑄𝑋 )
13 psmetcl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑄𝑋𝑥𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
14 11 12 10 13 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
15 14 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
16 6 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
17 16 rexrd ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ* )
18 4 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑅 ∈ ℝ* )
19 17 18 xaddcld ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) ∈ ℝ* )
20 19 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) ∈ ℝ* )
21 5 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → 𝑆 ∈ ℝ* )
22 2 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑃𝑋 )
23 psmetcl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋𝑥𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
24 11 22 10 23 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
25 17 24 xaddcld ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) ∈ ℝ* )
26 psmettri2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑃𝑋𝑄𝑋𝑥𝑋 ) ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) )
27 11 22 12 10 26 syl13anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) )
28 9 simplbda ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑥 ) < 𝑅 )
29 xltadd2 ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ*𝑅 ∈ ℝ* ∧ ( 𝑃 𝐷 𝑄 ) ∈ ℝ ) → ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ↔ ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) < ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) ) )
30 24 18 16 29 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ↔ ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) < ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) ) )
31 28 30 mpbid ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) < ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) )
32 14 25 19 27 31 xrlelttrd ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) < ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) )
33 32 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( 𝑄 𝐷 𝑥 ) < ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) )
34 5 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑆 ∈ ℝ* )
35 18 xnegcld ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → -𝑒 𝑅 ∈ ℝ* )
36 34 35 xaddcld ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) ∈ ℝ* )
37 7 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
38 xleadd1a ( ( ( ( 𝑃 𝐷 𝑄 ) ∈ ℝ* ∧ ( 𝑆 +𝑒 -𝑒 𝑅 ) ∈ ℝ*𝑅 ∈ ℝ* ) ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) ≤ ( ( 𝑆 +𝑒 -𝑒 𝑅 ) +𝑒 𝑅 ) )
39 17 36 18 37 38 syl31anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) ≤ ( ( 𝑆 +𝑒 -𝑒 𝑅 ) +𝑒 𝑅 ) )
40 39 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) ≤ ( ( 𝑆 +𝑒 -𝑒 𝑅 ) +𝑒 𝑅 ) )
41 xnpcan ( ( 𝑆 ∈ ℝ*𝑅 ∈ ℝ ) → ( ( 𝑆 +𝑒 -𝑒 𝑅 ) +𝑒 𝑅 ) = 𝑆 )
42 34 41 sylan ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑆 +𝑒 -𝑒 𝑅 ) +𝑒 𝑅 ) = 𝑆 )
43 40 42 breqtrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 𝑅 ) ≤ 𝑆 )
44 15 20 21 33 43 xrltletrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 ∈ ℝ ) → ( 𝑄 𝐷 𝑥 ) < 𝑆 )
45 14 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
46 6 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
47 simpll ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝜑 )
48 simplr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )
49 simpr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑅 = +∞ )
50 49 oveq2d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
51 48 50 eleqtrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
52 xblpnfps ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
53 1 2 52 syl2anc ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
54 53 simplbda ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ )
55 47 51 54 syl2anc ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ )
56 46 55 readdcld ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) ∈ ℝ )
57 56 rexrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) ∈ ℝ* )
58 pnfxr +∞ ∈ ℝ*
59 58 a1i ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → +∞ ∈ ℝ* )
60 1 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
61 2 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑃𝑋 )
62 3 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑄𝑋 )
63 10 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑥𝑋 )
64 60 61 62 63 26 syl13anc ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) )
65 46 55 rexaddd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) = ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) )
66 64 65 breqtrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) )
67 56 ltpnfd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) + ( 𝑃 𝐷 𝑥 ) ) < +∞ )
68 45 57 59 66 67 xrlelttrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) < +∞ )
69 0xr 0 ∈ ℝ*
70 69 a1i ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ∈ ℝ* )
71 psmetge0 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑄 ) )
72 11 22 12 71 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑃 𝐷 𝑄 ) )
73 70 17 36 72 37 xrletrd ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
74 ge0nemnf ( ( ( 𝑆 +𝑒 -𝑒 𝑅 ) ∈ ℝ* ∧ 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) ≠ -∞ )
75 36 73 74 syl2anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) ≠ -∞ )
76 75 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) ≠ -∞ )
77 5 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑆 ∈ ℝ* )
78 xaddmnf1 ( ( 𝑆 ∈ ℝ*𝑆 ≠ +∞ ) → ( 𝑆 +𝑒 -∞ ) = -∞ )
79 78 ex ( 𝑆 ∈ ℝ* → ( 𝑆 ≠ +∞ → ( 𝑆 +𝑒 -∞ ) = -∞ ) )
80 77 79 syl ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 ≠ +∞ → ( 𝑆 +𝑒 -∞ ) = -∞ ) )
81 xnegeq ( 𝑅 = +∞ → -𝑒 𝑅 = -𝑒 +∞ )
82 49 81 syl ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → -𝑒 𝑅 = -𝑒 +∞ )
83 xnegpnf -𝑒 +∞ = -∞
84 82 83 eqtrdi ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → -𝑒 𝑅 = -∞ )
85 84 oveq2d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( 𝑆 +𝑒 -∞ ) )
86 85 eqeq1d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑆 +𝑒 -𝑒 𝑅 ) = -∞ ↔ ( 𝑆 +𝑒 -∞ ) = -∞ ) )
87 80 86 sylibrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 ≠ +∞ → ( 𝑆 +𝑒 -𝑒 𝑅 ) = -∞ ) )
88 87 necon1d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑆 +𝑒 -𝑒 𝑅 ) ≠ -∞ → 𝑆 = +∞ ) )
89 76 88 mpd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑆 = +∞ )
90 68 89 breqtrrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) < 𝑆 )
91 psmetge0 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋𝑥𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) )
92 11 22 10 91 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) )
93 70 24 18 92 28 xrlelttrd ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 < 𝑅 )
94 70 18 93 xrltled ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ 𝑅 )
95 ge0nemnf ( ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ) → 𝑅 ≠ -∞ )
96 18 94 95 syl2anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑅 ≠ -∞ )
97 18 96 jca ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑅 ∈ ℝ*𝑅 ≠ -∞ ) )
98 xrnemnf ( ( 𝑅 ∈ ℝ*𝑅 ≠ -∞ ) ↔ ( 𝑅 ∈ ℝ ∨ 𝑅 = +∞ ) )
99 97 98 sylib ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑅 ∈ ℝ ∨ 𝑅 = +∞ ) )
100 44 90 99 mpjaodan ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) < 𝑆 )
101 elblps ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑄𝑋𝑆 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
102 11 12 34 101 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
103 10 100 102 mpbir2and ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )
104 103 ex ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
105 104 ssrdv ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )