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