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 ⊒ 𝐽 = ( MetOpen β€˜ 𝑀 )
ismtyhmeo.2 ⊒ 𝐾 = ( MetOpen β€˜ 𝑁 )
Assertion ismtyhmeo ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝑀 Ismty 𝑁 ) βŠ† ( 𝐽 Homeo 𝐾 ) )

Proof

Step Hyp Ref Expression
1 ismtyhmeo.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝑀 )
2 ismtyhmeo.2 ⊒ 𝐾 = ( MetOpen β€˜ 𝑁 )
3 simpll ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) β†’ 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) )
4 simplr ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) β†’ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) )
5 simpr ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) β†’ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) )
6 1 2 3 4 5 ismtyhmeolem ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) β†’ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
7 ismtycnv ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) β†’ β—‘ 𝑓 ∈ ( 𝑁 Ismty 𝑀 ) ) )
8 7 imp ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) β†’ β—‘ 𝑓 ∈ ( 𝑁 Ismty 𝑀 ) )
9 2 1 4 3 8 ismtyhmeolem ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) β†’ β—‘ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) )
10 ishmeo ⊒ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ↔ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ β—‘ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ) )
11 6 9 10 sylanbrc ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) β†’ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) )
12 11 ex ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) β†’ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) )
13 12 ssrdv ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝑀 Ismty 𝑁 ) βŠ† ( 𝐽 Homeo 𝐾 ) )