| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ovex |
|- ( RR* ^m ( x X. x ) ) e. _V |
| 2 |
1
|
rabex |
|- { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } e. _V |
| 3 |
|
df-xmet |
|- *Met = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } ) |
| 4 |
2 3
|
fnmpti |
|- *Met Fn _V |
| 5 |
|
fnunirn |
|- ( *Met Fn _V -> ( D e. U. ran *Met <-> E. x e. _V D e. ( *Met ` x ) ) ) |
| 6 |
4 5
|
ax-mp |
|- ( D e. U. ran *Met <-> E. x e. _V D e. ( *Met ` x ) ) |
| 7 |
|
id |
|- ( D e. ( *Met ` x ) -> D e. ( *Met ` x ) ) |
| 8 |
|
xmetdmdm |
|- ( D e. ( *Met ` x ) -> x = dom dom D ) |
| 9 |
8
|
fveq2d |
|- ( D e. ( *Met ` x ) -> ( *Met ` x ) = ( *Met ` dom dom D ) ) |
| 10 |
7 9
|
eleqtrd |
|- ( D e. ( *Met ` x ) -> D e. ( *Met ` dom dom D ) ) |
| 11 |
10
|
rexlimivw |
|- ( E. x e. _V D e. ( *Met ` x ) -> D e. ( *Met ` dom dom D ) ) |
| 12 |
6 11
|
sylbi |
|- ( D e. U. ran *Met -> D e. ( *Met ` dom dom D ) ) |
| 13 |
|
fvssunirn |
|- ( *Met ` dom dom D ) C_ U. ran *Met |
| 14 |
13
|
sseli |
|- ( D e. ( *Met ` dom dom D ) -> D e. U. ran *Met ) |
| 15 |
12 14
|
impbii |
|- ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) ) |