Step |
Hyp |
Ref |
Expression |
1 |
|
blf |
|- ( D e. ( *Met ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X ) |
2 |
1
|
frnd |
|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ ~P X ) |
3 |
|
sspwuni |
|- ( ran ( ball ` D ) C_ ~P X <-> U. ran ( ball ` D ) C_ X ) |
4 |
2 3
|
sylib |
|- ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) C_ X ) |
5 |
|
1rp |
|- 1 e. RR+ |
6 |
|
blcntr |
|- ( ( D e. ( *Met ` X ) /\ x e. X /\ 1 e. RR+ ) -> x e. ( x ( ball ` D ) 1 ) ) |
7 |
5 6
|
mp3an3 |
|- ( ( D e. ( *Met ` X ) /\ x e. X ) -> x e. ( x ( ball ` D ) 1 ) ) |
8 |
|
1xr |
|- 1 e. RR* |
9 |
|
blelrn |
|- ( ( D e. ( *Met ` X ) /\ x e. X /\ 1 e. RR* ) -> ( x ( ball ` D ) 1 ) e. ran ( ball ` D ) ) |
10 |
8 9
|
mp3an3 |
|- ( ( D e. ( *Met ` X ) /\ x e. X ) -> ( x ( ball ` D ) 1 ) e. ran ( ball ` D ) ) |
11 |
|
elunii |
|- ( ( x e. ( x ( ball ` D ) 1 ) /\ ( x ( ball ` D ) 1 ) e. ran ( ball ` D ) ) -> x e. U. ran ( ball ` D ) ) |
12 |
7 10 11
|
syl2anc |
|- ( ( D e. ( *Met ` X ) /\ x e. X ) -> x e. U. ran ( ball ` D ) ) |
13 |
4 12
|
eqelssd |
|- ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) = X ) |