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 \in ∞Met (X) \land N \in ∞Met (Y)) \to M Ismty N \subseteq J Homeo K$

Proof

Step	Hyp	Ref	Expression
1		ismtyhmeo.1	$⊢ J = MetOpen (M)$
2		ismtyhmeo.2	$⊢ K = MetOpen (N)$
3		simpll	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land f \in (M Ismty N)) \to M \in ∞Met (X)$
4		simplr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land f \in (M Ismty N)) \to N \in ∞Met (Y)$
5		simpr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land f \in (M Ismty N)) \to f \in (M Ismty N)$
6	1 2 3 4 5	ismtyhmeolem	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land f \in (M Ismty N)) \to f \in (J Cn K)$
7		ismtycnv	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (f \in (M Ismty N) \to f^{-1} \in (N Ismty M))$
8	7	imp	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land f \in (M Ismty N)) \to f^{-1} \in (N Ismty M)$
9	2 1 4 3 8	ismtyhmeolem	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land f \in (M Ismty N)) \to f^{-1} \in (K Cn J)$
10		ishmeo	$⊢ f \in (J Homeo K) \leftrightarrow (f \in (J Cn K) \land f^{-1} \in (K Cn J))$
11	6 9 10	sylanbrc	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y)) \land f \in (M Ismty N)) \to f \in (J Homeo K)$
12	11	ex	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (f \in (M Ismty N) \to f \in (J Homeo K))$
13	12	ssrdv	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to M Ismty N \subseteq J Homeo K$