Step |
Hyp |
Ref |
Expression |
1 |
|
n0 |
⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) |
2 |
|
elbl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) ) |
3 |
|
xmetge0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) ) |
4 |
3
|
3expa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) ) |
5 |
4
|
3adantl3 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) ) |
6 |
|
0xr |
⊢ 0 ∈ ℝ* |
7 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ) |
8 |
7
|
3expa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ) |
9 |
8
|
3adantl3 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ) |
10 |
|
simpl3 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ* ) |
11 |
|
xrlelttr |
⊢ ( ( 0 ∈ ℝ* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( ( 0 ≤ ( 𝑃 𝐷 𝑥 ) ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) → 0 < 𝑅 ) ) |
12 |
6 9 10 11
|
mp3an2i |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 0 ≤ ( 𝑃 𝐷 𝑥 ) ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) → 0 < 𝑅 ) ) |
13 |
5 12
|
mpand |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) < 𝑅 → 0 < 𝑅 ) ) |
14 |
13
|
expimpd |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) → 0 < 𝑅 ) ) |
15 |
2 14
|
sylbid |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → 0 < 𝑅 ) ) |
16 |
15
|
exlimdv |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ∃ 𝑥 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → 0 < 𝑅 ) ) |
17 |
1 16
|
syl5bi |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ≠ ∅ → 0 < 𝑅 ) ) |
18 |
|
xblcntr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) |
19 |
18
|
ne0d |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ≠ ∅ ) |
20 |
19
|
3expa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ≠ ∅ ) |
21 |
20
|
expr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( 0 < 𝑅 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ≠ ∅ ) ) |
22 |
21
|
3impa |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 0 < 𝑅 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ≠ ∅ ) ) |
23 |
17 22
|
impbid |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ≠ ∅ ↔ 0 < 𝑅 ) ) |