Metamath Proof Explorer


Theorem ismtybndlem

Description: Lemma for ismtybnd . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 19-Jan-2014)

Ref Expression
Assertion ismtybndlem
|- ( ( N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( M e. ( Bnd ` X ) -> N e. ( Bnd ` Y ) ) )

Proof

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 ) ) )