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 e. ( PsMet ` X ) /\ P e. X ) -> ( A e. ( P ( ball ` D ) +oo ) <-> ( A e. X /\ ( P D A ) e. RR ) ) )

Proof

Step Hyp Ref Expression
1 pnfxr
 |-  +oo e. RR*
2 elblps
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ +oo e. RR* ) -> ( A e. ( P ( ball ` D ) +oo ) <-> ( A e. X /\ ( P D A ) < +oo ) ) )
3 1 2 mp3an3
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( A e. ( P ( ball ` D ) +oo ) <-> ( A e. X /\ ( P D A ) < +oo ) ) )
4 psmetcl
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> ( P D A ) e. RR* )
5 psmetge0
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> 0 <_ ( P D A ) )
6 ge0nemnf
 |-  ( ( ( P D A ) e. RR* /\ 0 <_ ( P D A ) ) -> ( P D A ) =/= -oo )
7 4 5 6 syl2anc
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> ( P D A ) =/= -oo )
8 ngtmnft
 |-  ( ( P D A ) e. RR* -> ( ( P D A ) = -oo <-> -. -oo < ( P D A ) ) )
9 4 8 syl
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> ( ( P D A ) = -oo <-> -. -oo < ( P D A ) ) )
10 9 necon2abid
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> ( -oo < ( P D A ) <-> ( P D A ) =/= -oo ) )
11 7 10 mpbird
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> -oo < ( P D A ) )
12 11 biantrurd
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> ( ( P D A ) < +oo <-> ( -oo < ( P D A ) /\ ( P D A ) < +oo ) ) )
13 xrrebnd
 |-  ( ( P D A ) e. RR* -> ( ( P D A ) e. RR <-> ( -oo < ( P D A ) /\ ( P D A ) < +oo ) ) )
14 4 13 syl
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> ( ( P D A ) e. RR <-> ( -oo < ( P D A ) /\ ( P D A ) < +oo ) ) )
15 12 14 bitr4d
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ A e. X ) -> ( ( P D A ) < +oo <-> ( P D A ) e. RR ) )
16 15 3expa
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ A e. X ) -> ( ( P D A ) < +oo <-> ( P D A ) e. RR ) )
17 16 pm5.32da
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( ( A e. X /\ ( P D A ) < +oo ) <-> ( A e. X /\ ( P D A ) e. RR ) ) )
18 3 17 bitrd
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( A e. ( P ( ball ` D ) +oo ) <-> ( A e. X /\ ( P D A ) e. RR ) ) )