Step |
Hyp |
Ref |
Expression |
1 |
|
0xr |
⊢ 0 ∈ ℝ* |
2 |
1
|
a1i |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ∈ ℝ* ) |
3 |
|
simpl1 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
4 |
|
simpl2 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑃 ∈ 𝑋 ) |
5 |
|
elbl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) < 𝑅 ) ) ) |
6 |
5
|
simprbda |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝐴 ∈ 𝑋 ) |
7 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑃 𝐷 𝐴 ) ∈ ℝ* ) |
8 |
3 4 6 7
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝐴 ) ∈ ℝ* ) |
9 |
|
simpl3 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑅 ∈ ℝ* ) |
10 |
|
xmetge0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝐴 ) ) |
11 |
3 4 6 10
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑃 𝐷 𝐴 ) ) |
12 |
5
|
simplbda |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝐴 ) < 𝑅 ) |
13 |
2 8 9 11 12
|
xrlelttrd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 < 𝑅 ) |