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)
Ref | Expression | ||
---|---|---|---|
Assertion | blrn | |- ( D e. ( *Met ` X ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | blf | |- ( D e. ( *Met ` 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. ( *Met ` X ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) ) |