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