Step |
Hyp |
Ref |
Expression |
1 |
|
simpl1 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) |
2 |
|
simpl2 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑃 ∈ 𝑋 ) |
3 |
|
simpl3 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑄 ∈ 𝑋 ) |
4 |
|
simpr1 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑅 ∈ ℝ ) |
5 |
4
|
rexrd |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑅 ∈ ℝ* ) |
6 |
|
simpr2 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑆 ∈ ℝ ) |
7 |
6
|
rexrd |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑆 ∈ ℝ* ) |
8 |
6 4
|
resubcld |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑆 − 𝑅 ) ∈ ℝ ) |
9 |
|
simpr3 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) |
10 |
|
psmetlecl |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( ( 𝑆 − 𝑅 ) ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ ) |
11 |
1 2 3 8 9 10
|
syl122anc |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ ) |
12 |
|
rexsub |
⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( 𝑆 − 𝑅 ) ) |
13 |
6 4 12
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( 𝑆 − 𝑅 ) ) |
14 |
9 13
|
breqtrrd |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ) |
15 |
1 2 3 5 7 11 14
|
xblss2ps |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) |