Metamath Proof Explorer

Theorem xblpnf

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)

Ref Expression
Assertion xblpnf 
|- ( ( D e. ( *Met ` 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 elbl 
 |-  ( ( D e. ( *Met ` 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. ( *Met ` X ) /\ P e. X ) -> ( A e. ( P ( ball ` D ) +oo ) <-> ( A e. X /\ ( P D A ) < +oo ) ) )
4 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. X ) -> ( P D A ) e. RR* )
5 xmetge0 
 |-  ( ( D e. ( *Met ` 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. ( *Met ` 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. ( *Met ` X ) /\ P e. X /\ A e. X ) -> ( ( P D A ) = -oo <-> -. -oo < ( P D A ) ) )
10 9 necon2abid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. X ) -> ( -oo < ( P D A ) <-> ( P D A ) =/= -oo ) )
11 7 10 mpbird 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. X ) -> -oo < ( P D A ) )
12 11 biantrurd 
 |-  ( ( D e. ( *Met ` 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. ( *Met ` 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. ( *Met ` X ) /\ P e. X /\ A e. X ) -> ( ( P D A ) < +oo <-> ( P D A ) e. RR ) )
16 15 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ A e. X ) -> ( ( P D A ) < +oo <-> ( P D A ) e. RR ) )
17 16 pm5.32da 
 |-  ( ( D e. ( *Met ` 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. ( *Met ` X ) /\ P e. X ) -> ( A e. ( P ( ball ` D ) +oo ) <-> ( A e. X /\ ( P D A ) e. RR ) ) )