Metamath Proof Explorer


Theorem xblss2

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)

Ref Expression
Hypotheses xblss2.1 ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
xblss2.2 ( 𝜑𝑃𝑋 )
xblss2.3 ( 𝜑𝑄𝑋 )
xblss2.4 ( 𝜑𝑅 ∈ ℝ* )
xblss2.5 ( 𝜑𝑆 ∈ ℝ* )
xblss2.6 ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
xblss2.7 ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
Assertion xblss2 ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )

Proof

Step Hyp Ref Expression
1 xblss2.1 ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2 xblss2.2 ( 𝜑𝑃𝑋 )
3 xblss2.3 ( 𝜑𝑄𝑋 )
4 xblss2.4 ( 𝜑𝑅 ∈ ℝ* )
5 xblss2.5 ( 𝜑𝑆 ∈ ℝ* )
6 xblss2.6 ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
7 xblss2.7 ( 𝜑 → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
8 elbl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
9 1 2 4 8 syl3anc ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
10 9 simprbda ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥𝑋 )
11 1 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
12 3 adantr ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑄𝑋 )
13 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄𝑋𝑥𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
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 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑥𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
24 11 22 10 23 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
25 17 24 xaddcld ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) ∈ ℝ* )
26 xmettri2 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑃𝑋𝑄𝑋𝑥𝑋 ) ) → ( 𝑄 𝐷 𝑥 ) ≤ ( ( 𝑃 𝐷 𝑄 ) +𝑒 ( 𝑃 𝐷 𝑥 ) ) )
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 28 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 𝐷 𝑥 ) < 𝑅 )
46 7 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
47 0xr 0 ∈ ℝ*
48 47 a1i ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ∈ ℝ* )
49 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑄 ) )
50 11 22 12 49 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑃 𝐷 𝑄 ) )
51 48 17 36 50 37 xrletrd ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
52 ge0nemnf ( ( ( 𝑆 +𝑒 -𝑒 𝑅 ) ∈ ℝ* ∧ 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) ≠ -∞ )
53 36 51 52 syl2anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) ≠ -∞ )
54 53 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) ≠ -∞ )
55 5 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑆 ∈ ℝ* )
56 xaddmnf1 ( ( 𝑆 ∈ ℝ*𝑆 ≠ +∞ ) → ( 𝑆 +𝑒 -∞ ) = -∞ )
57 56 ex ( 𝑆 ∈ ℝ* → ( 𝑆 ≠ +∞ → ( 𝑆 +𝑒 -∞ ) = -∞ ) )
58 55 57 syl ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 ≠ +∞ → ( 𝑆 +𝑒 -∞ ) = -∞ ) )
59 simpr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑅 = +∞ )
60 xnegeq ( 𝑅 = +∞ → -𝑒 𝑅 = -𝑒 +∞ )
61 59 60 syl ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → -𝑒 𝑅 = -𝑒 +∞ )
62 xnegpnf -𝑒 +∞ = -∞
63 61 62 eqtrdi ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → -𝑒 𝑅 = -∞ )
64 63 oveq2d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( 𝑆 +𝑒 -∞ ) )
65 64 eqeq1d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑆 +𝑒 -𝑒 𝑅 ) = -∞ ↔ ( 𝑆 +𝑒 -∞ ) = -∞ ) )
66 58 65 sylibrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 ≠ +∞ → ( 𝑆 +𝑒 -𝑒 𝑅 ) = -∞ ) )
67 66 necon1d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑆 +𝑒 -𝑒 𝑅 ) ≠ -∞ → 𝑆 = +∞ ) )
68 54 67 mpd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑆 = +∞ )
69 68 63 oveq12d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( +∞ +𝑒 -∞ ) )
70 pnfaddmnf ( +∞ +𝑒 -∞ ) = 0
71 69 70 eqtrdi ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = 0 )
72 46 71 breqtrd ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 𝐷 𝑄 ) ≤ 0 )
73 50 biantrud ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) ≤ 0 ↔ ( ( 𝑃 𝐷 𝑄 ) ≤ 0 ∧ 0 ≤ ( 𝑃 𝐷 𝑄 ) ) ) )
74 xrletri3 ( ( ( 𝑃 𝐷 𝑄 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝑃 𝐷 𝑄 ) = 0 ↔ ( ( 𝑃 𝐷 𝑄 ) ≤ 0 ∧ 0 ≤ ( 𝑃 𝐷 𝑄 ) ) ) )
75 17 47 74 sylancl ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) = 0 ↔ ( ( 𝑃 𝐷 𝑄 ) ≤ 0 ∧ 0 ≤ ( 𝑃 𝐷 𝑄 ) ) ) )
76 xmeteq0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) → ( ( 𝑃 𝐷 𝑄 ) = 0 ↔ 𝑃 = 𝑄 ) )
77 11 22 12 76 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) = 0 ↔ 𝑃 = 𝑄 ) )
78 73 75 77 3bitr2d ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( ( 𝑃 𝐷 𝑄 ) ≤ 0 ↔ 𝑃 = 𝑄 ) )
79 78 adantr ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( ( 𝑃 𝐷 𝑄 ) ≤ 0 ↔ 𝑃 = 𝑄 ) )
80 72 79 mpbid ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑃 = 𝑄 )
81 80 oveq1d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑃 𝐷 𝑥 ) = ( 𝑄 𝐷 𝑥 ) )
82 59 68 eqtr4d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → 𝑅 = 𝑆 )
83 45 81 82 3brtr3d ( ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ∧ 𝑅 = +∞ ) → ( 𝑄 𝐷 𝑥 ) < 𝑆 )
84 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑥𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) )
85 11 22 10 84 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) )
86 48 24 18 85 28 xrlelttrd ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 < 𝑅 )
87 48 18 86 xrltled ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ 𝑅 )
88 ge0nemnf ( ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ) → 𝑅 ≠ -∞ )
89 18 87 88 syl2anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑅 ≠ -∞ )
90 18 89 jca ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑅 ∈ ℝ*𝑅 ≠ -∞ ) )
91 xrnemnf ( ( 𝑅 ∈ ℝ*𝑅 ≠ -∞ ) ↔ ( 𝑅 ∈ ℝ ∨ 𝑅 = +∞ ) )
92 90 91 sylib ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑅 ∈ ℝ ∨ 𝑅 = +∞ ) )
93 44 83 92 mpjaodan ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑄 𝐷 𝑥 ) < 𝑆 )
94 elbl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄𝑋𝑆 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
95 11 12 34 94 syl3anc ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
96 10 93 95 mpbir2and ( ( 𝜑𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )
97 96 ex ( 𝜑 → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
98 97 ssrdv ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )