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 β€˜ 𝐷 ) 𝑆 ) )