Metamath Proof Explorer

Theorem blpnf

Description: The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion blpnf 
|- ( ( D e. ( Met ` X ) /\ P e. X ) -> ( P ( ball ` D ) +oo ) = X )

Proof

Step Hyp Ref Expression
1 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
2 xblpnf 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( x e. ( P ( ball ` D ) +oo ) <-> ( x e. X /\ ( P D x ) e. RR ) ) )
3 1 2 sylan 
 |-  ( ( D e. ( Met ` X ) /\ P e. X ) -> ( x e. ( P ( ball ` D ) +oo ) <-> ( x e. X /\ ( P D x ) e. RR ) ) )
4 metcl 
 |-  ( ( D e. ( Met ` X ) /\ P e. X /\ x e. X ) -> ( P D x ) e. RR )
5 4 3expia 
 |-  ( ( D e. ( Met ` X ) /\ P e. X ) -> ( x e. X -> ( P D x ) e. RR ) )
6 5 pm4.71d 
 |-  ( ( D e. ( Met ` X ) /\ P e. X ) -> ( x e. X <-> ( x e. X /\ ( P D x ) e. RR ) ) )
7 3 6 bitr4d 
 |-  ( ( D e. ( Met ` X ) /\ P e. X ) -> ( x e. ( P ( ball ` D ) +oo ) <-> x e. X ) )
8 7 eqrdv 
 |-  ( ( D e. ( Met ` X ) /\ P e. X ) -> ( P ( ball ` D ) +oo ) = X )