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