This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐷 ) 𝑆 ) )