Step |
Hyp |
Ref |
Expression |
1 |
|
isismty |
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) <-> ( F : X -1-1-onto-> Y /\ A. z e. X A. w e. X ( z M w ) = ( ( F ` z ) N ( F ` w ) ) ) ) ) |
2 |
1
|
biimp3a |
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( F : X -1-1-onto-> Y /\ A. z e. X A. w e. X ( z M w ) = ( ( F ` z ) N ( F ` w ) ) ) ) |
3 |
2
|
simpld |
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> F : X -1-1-onto-> Y ) |
4 |
|
f1ocnv |
|- ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X ) |
5 |
|
f1of |
|- ( `' F : Y -1-1-onto-> X -> `' F : Y --> X ) |
6 |
3 4 5
|
3syl |
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> `' F : Y --> X ) |
7 |
6
|
ffvelrnda |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ y e. Y ) -> ( `' F ` y ) e. X ) |
8 |
|
oveq1 |
|- ( x = ( `' F ` y ) -> ( x ( ball ` M ) r ) = ( ( `' F ` y ) ( ball ` M ) r ) ) |
9 |
8
|
eqeq2d |
|- ( x = ( `' F ` y ) -> ( X = ( x ( ball ` M ) r ) <-> X = ( ( `' F ` y ) ( ball ` M ) r ) ) ) |
10 |
9
|
rexbidv |
|- ( x = ( `' F ` y ) -> ( E. r e. RR+ X = ( x ( ball ` M ) r ) <-> E. r e. RR+ X = ( ( `' F ` y ) ( ball ` M ) r ) ) ) |
11 |
10
|
rspcv |
|- ( ( `' F ` y ) e. X -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> E. r e. RR+ X = ( ( `' F ` y ) ( ball ` M ) r ) ) ) |
12 |
7 11
|
syl |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ y e. Y ) -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> E. r e. RR+ X = ( ( `' F ` y ) ( ball ` M ) r ) ) ) |
13 |
|
imaeq2 |
|- ( X = ( ( `' F ` y ) ( ball ` M ) r ) -> ( F " X ) = ( F " ( ( `' F ` y ) ( ball ` M ) r ) ) ) |
14 |
|
f1ofo |
|- ( F : X -1-1-onto-> Y -> F : X -onto-> Y ) |
15 |
|
foima |
|- ( F : X -onto-> Y -> ( F " X ) = Y ) |
16 |
3 14 15
|
3syl |
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( F " X ) = Y ) |
17 |
16
|
adantr |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( y e. Y /\ r e. RR+ ) ) -> ( F " X ) = Y ) |
18 |
|
rpxr |
|- ( r e. RR+ -> r e. RR* ) |
19 |
18
|
adantl |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ r e. RR+ ) -> r e. RR* ) |
20 |
7 19
|
anim12dan |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( y e. Y /\ r e. RR+ ) ) -> ( ( `' F ` y ) e. X /\ r e. RR* ) ) |
21 |
|
ismtyima |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( ( `' F ` y ) e. X /\ r e. RR* ) ) -> ( F " ( ( `' F ` y ) ( ball ` M ) r ) ) = ( ( F ` ( `' F ` y ) ) ( ball ` N ) r ) ) |
22 |
20 21
|
syldan |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( y e. Y /\ r e. RR+ ) ) -> ( F " ( ( `' F ` y ) ( ball ` M ) r ) ) = ( ( F ` ( `' F ` y ) ) ( ball ` N ) r ) ) |
23 |
|
simpl |
|- ( ( y e. Y /\ r e. RR+ ) -> y e. Y ) |
24 |
|
f1ocnvfv2 |
|- ( ( F : X -1-1-onto-> Y /\ y e. Y ) -> ( F ` ( `' F ` y ) ) = y ) |
25 |
3 23 24
|
syl2an |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( y e. Y /\ r e. RR+ ) ) -> ( F ` ( `' F ` y ) ) = y ) |
26 |
25
|
oveq1d |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( y e. Y /\ r e. RR+ ) ) -> ( ( F ` ( `' F ` y ) ) ( ball ` N ) r ) = ( y ( ball ` N ) r ) ) |
27 |
22 26
|
eqtrd |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( y e. Y /\ r e. RR+ ) ) -> ( F " ( ( `' F ` y ) ( ball ` M ) r ) ) = ( y ( ball ` N ) r ) ) |
28 |
17 27
|
eqeq12d |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( y e. Y /\ r e. RR+ ) ) -> ( ( F " X ) = ( F " ( ( `' F ` y ) ( ball ` M ) r ) ) <-> Y = ( y ( ball ` N ) r ) ) ) |
29 |
13 28
|
syl5ib |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( y e. Y /\ r e. RR+ ) ) -> ( X = ( ( `' F ` y ) ( ball ` M ) r ) -> Y = ( y ( ball ` N ) r ) ) ) |
30 |
29
|
anassrs |
|- ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ y e. Y ) /\ r e. RR+ ) -> ( X = ( ( `' F ` y ) ( ball ` M ) r ) -> Y = ( y ( ball ` N ) r ) ) ) |
31 |
30
|
reximdva |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ y e. Y ) -> ( E. r e. RR+ X = ( ( `' F ` y ) ( ball ` M ) r ) -> E. r e. RR+ Y = ( y ( ball ` N ) r ) ) ) |
32 |
12 31
|
syld |
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ y e. Y ) -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> E. r e. RR+ Y = ( y ( ball ` N ) r ) ) ) |
33 |
32
|
ralrimdva |
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> A. y e. Y E. r e. RR+ Y = ( y ( ball ` N ) r ) ) ) |
34 |
|
simp2 |
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> N e. ( *Met ` Y ) ) |
35 |
33 34
|
jctild |
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> ( N e. ( *Met ` Y ) /\ A. y e. Y E. r e. RR+ Y = ( y ( ball ` N ) r ) ) ) ) |
36 |
35
|
3expib |
|- ( M e. ( *Met ` X ) -> ( ( N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> ( N e. ( *Met ` Y ) /\ A. y e. Y E. r e. RR+ Y = ( y ( ball ` N ) r ) ) ) ) ) |
37 |
36
|
com12 |
|- ( ( N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( M e. ( *Met ` X ) -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> ( N e. ( *Met ` Y ) /\ A. y e. Y E. r e. RR+ Y = ( y ( ball ` N ) r ) ) ) ) ) |
38 |
37
|
impd |
|- ( ( N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( ( M e. ( *Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) -> ( N e. ( *Met ` Y ) /\ A. y e. Y E. r e. RR+ Y = ( y ( ball ` N ) r ) ) ) ) |
39 |
|
isbndx |
|- ( M e. ( Bnd ` X ) <-> ( M e. ( *Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) ) |
40 |
|
isbndx |
|- ( N e. ( Bnd ` Y ) <-> ( N e. ( *Met ` Y ) /\ A. y e. Y E. r e. RR+ Y = ( y ( ball ` N ) r ) ) ) |
41 |
38 39 40
|
3imtr4g |
|- ( ( N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( M e. ( Bnd ` X ) -> N e. ( Bnd ` Y ) ) ) |