Step |
Hyp |
Ref |
Expression |
1 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
2 |
|
elbl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ +∞ ∈ ℝ* ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) ) |
3 |
1 2
|
mp3an3 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) ) |
4 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑃 𝐷 𝐴 ) ∈ ℝ* ) |
5 |
|
xmetge0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝐴 ) ) |
6 |
|
ge0nemnf |
⊢ ( ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝐴 ) ) → ( 𝑃 𝐷 𝐴 ) ≠ -∞ ) |
7 |
4 5 6
|
syl2anc |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑃 𝐷 𝐴 ) ≠ -∞ ) |
8 |
|
ngtmnft |
⊢ ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ* → ( ( 𝑃 𝐷 𝐴 ) = -∞ ↔ ¬ -∞ < ( 𝑃 𝐷 𝐴 ) ) ) |
9 |
4 8
|
syl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) = -∞ ↔ ¬ -∞ < ( 𝑃 𝐷 𝐴 ) ) ) |
10 |
9
|
necon2abid |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( -∞ < ( 𝑃 𝐷 𝐴 ) ↔ ( 𝑃 𝐷 𝐴 ) ≠ -∞ ) ) |
11 |
7 10
|
mpbird |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → -∞ < ( 𝑃 𝐷 𝐴 ) ) |
12 |
11
|
biantrurd |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) < +∞ ↔ ( -∞ < ( 𝑃 𝐷 𝐴 ) ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) ) |
13 |
|
xrrebnd |
⊢ ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ* → ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ ↔ ( -∞ < ( 𝑃 𝐷 𝐴 ) ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) ) |
14 |
4 13
|
syl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ ↔ ( -∞ < ( 𝑃 𝐷 𝐴 ) ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) ) |
15 |
12 14
|
bitr4d |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) < +∞ ↔ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) |
16 |
15
|
3expa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) < +∞ ↔ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) |
17 |
16
|
pm5.32da |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) ) |
18 |
3 17
|
bitrd |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) ) |