Metamath Proof Explorer

Theorem ismtybnd

Description: Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 19-Jan-2014)

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

Proof

Step Hyp Ref Expression
1 ismtybndlem 
 |-  ( ( N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( M e. ( Bnd ` X ) -> N e. ( Bnd ` Y ) ) )
2 1 3adant1 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( M e. ( Bnd ` X ) -> N e. ( Bnd ` Y ) ) )
3 ismtycnv 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) -> `' F e. ( N Ismty M ) ) )
4 3 3impia 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> `' F e. ( N Ismty M ) )
5 ismtybndlem 
 |-  ( ( M e. ( *Met ` X ) /\ `' F e. ( N Ismty M ) ) -> ( N e. ( Bnd ` Y ) -> M e. ( Bnd ` X ) ) )
6 5 3adant2 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ `' F e. ( N Ismty M ) ) -> ( N e. ( Bnd ` Y ) -> M e. ( Bnd ` X ) ) )
7 4 6 syld3an3 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( N e. ( Bnd ` Y ) -> M e. ( Bnd ` X ) ) )
8 2 7 impbid 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( M e. ( Bnd ` X ) <-> N e. ( Bnd ` Y ) ) )