Step |
Hyp |
Ref |
Expression |
1 |
|
simp1l |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) |
2 |
|
simp1r |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝑃 ∈ 𝑋 ) |
3 |
|
simp2l |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝑅 ∈ ℝ* ) |
4 |
|
simp2r |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝑆 ∈ ℝ* ) |
5 |
|
psmet0 |
⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑃 ) = 0 ) |
6 |
5
|
3ad2ant1 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 𝐷 𝑃 ) = 0 ) |
7 |
|
0re |
⊢ 0 ∈ ℝ |
8 |
6 7
|
eqeltrdi |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 𝐷 𝑃 ) ∈ ℝ ) |
9 |
|
simp3 |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝑅 ≤ 𝑆 ) |
10 |
|
xsubge0 |
⊢ ( ( 𝑆 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ↔ 𝑅 ≤ 𝑆 ) ) |
11 |
4 3 10
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ↔ 𝑅 ≤ 𝑆 ) ) |
12 |
9 11
|
mpbird |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ) |
13 |
6 12
|
eqbrtrd |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 𝐷 𝑃 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ) |
14 |
1 2 2 3 4 8 13
|
xblss2ps |
⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) |