Metamath Proof Explorer

Theorem ismtyhmeo

Description: An isometry is a homeomorphism on the induced topology. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses ismtyhmeo.1 
|- J = ( MetOpen ` M )
ismtyhmeo.2 
|- K = ( MetOpen ` N )
Assertion ismtyhmeo 
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( M Ismty N ) C_ ( J Homeo K ) )

Proof

Step Hyp Ref Expression
1 ismtyhmeo.1 
 |-  J = ( MetOpen ` M )
2 ismtyhmeo.2 
 |-  K = ( MetOpen ` N )
3 simpll 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ f e. ( M Ismty N ) ) -> M e. ( *Met ` X ) )
4 simplr 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ f e. ( M Ismty N ) ) -> N e. ( *Met ` Y ) )
5 simpr 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ f e. ( M Ismty N ) ) -> f e. ( M Ismty N ) )
6 1 2 3 4 5 ismtyhmeolem 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ f e. ( M Ismty N ) ) -> f e. ( J Cn K ) )
7 ismtycnv 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( f e. ( M Ismty N ) -> `' f e. ( N Ismty M ) ) )
8 7 imp 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ f e. ( M Ismty N ) ) -> `' f e. ( N Ismty M ) )
9 2 1 4 3 8 ismtyhmeolem 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ f e. ( M Ismty N ) ) -> `' f e. ( K Cn J ) )
10 ishmeo 
 |-  ( f e. ( J Homeo K ) <-> ( f e. ( J Cn K ) /\ `' f e. ( K Cn J ) ) )
11 6 9 10 sylanbrc 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ f e. ( M Ismty N ) ) -> f e. ( J Homeo K ) )
12 11 ex 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( f e. ( M Ismty N ) -> f e. ( J Homeo K ) ) )
13 12 ssrdv 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( M Ismty N ) C_ ( J Homeo K ) )