Metamath Proof Explorer


Theorem blrnps

Description: Membership in the range of the ball function. Note that ran ( ballD ) is the collection of all balls for metric D . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blrnps
|- ( D e. ( PsMet ` X ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) )

Proof

Step Hyp Ref Expression
1 blfps
 |-  ( D e. ( PsMet ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )
2 ffn
 |-  ( ( ball ` D ) : ( X X. RR* ) --> ~P X -> ( ball ` D ) Fn ( X X. RR* ) )
3 ovelrn
 |-  ( ( ball ` D ) Fn ( X X. RR* ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) )
4 1 2 3 3syl
 |-  ( D e. ( PsMet ` X ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) )