Metamath Proof Explorer

Theorem xblpnfps

Description: The infinity ball in an extended metric is the set of all points that are a finite distance from the center. (Contributed by Mario Carneiro, 23-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion xblpnfps ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X → A ∈ P ball ⁡ D +∞ ↔ A ∈ X ∧ P D A ∈ ℝ

Proof

Step Hyp Ref Expression
1 pnfxr ⊢ +∞ ∈ ℝ *
2 elblps ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ +∞ ∈ ℝ * → A ∈ P ball ⁡ D +∞ ↔ A ∈ X ∧ P D A < +∞
3 1 2 mp3an3 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X → A ∈ P ball ⁡ D +∞ ↔ A ∈ X ∧ P D A < +∞
4 psmetcl ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A ∈ ℝ *
5 psmetge0 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → 0 ≤ P D A
6 ge0nemnf ⊢ P D A ∈ ℝ * ∧ 0 ≤ P D A → P D A ≠ −∞
7 4 5 6 syl2anc ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A ≠ −∞
8 ngtmnft ⊢ P D A ∈ ℝ * → P D A = −∞ ↔ ¬ −∞ < P D A
9 4 8 syl ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A = −∞ ↔ ¬ −∞ < P D A
10 9 necon2abid ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → −∞ < P D A ↔ P D A ≠ −∞
11 7 10 mpbird ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → −∞ < P D A
12 11 biantrurd ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A < +∞ ↔ −∞ < P D A ∧ P D A < +∞
13 xrrebnd ⊢ P D A ∈ ℝ * → P D A ∈ ℝ ↔ −∞ < P D A ∧ P D A < +∞
14 4 13 syl ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A ∈ ℝ ↔ −∞ < P D A ∧ P D A < +∞
15 12 14 bitr4d ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A < +∞ ↔ P D A ∈ ℝ
16 15 3expa ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A < +∞ ↔ P D A ∈ ℝ
17 16 pm5.32da ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X → A ∈ X ∧ P D A < +∞ ↔ A ∈ X ∧ P D A ∈ ℝ
18 3 17 bitrd ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X → A ∈ P ball ⁡ D +∞ ↔ A ∈ X ∧ P D A ∈ ℝ