ismtybnd

Description: Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 19-Jan-2014)

		Ref	Expression
	Assertion	ismtybnd	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to (M \in Bnd (X) \leftrightarrow N \in Bnd (Y))$

Step	Hyp	Ref	Expression
1		ismtybndlem	$⊢ (N \in ∞Met (Y) \land F \in (M Ismty N)) \to (M \in Bnd (X) \to N \in Bnd (Y))$
2	1	3adant1	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to (M \in Bnd (X) \to N \in Bnd (Y))$
3		ismtycnv	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in (M Ismty N) \to F^{-1} \in (N Ismty M))$
4	3	3impia	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to F^{-1} \in (N Ismty M)$
5		ismtybndlem	$⊢ (M \in ∞Met (X) \land F^{-1} \in (N Ismty M)) \to (N \in Bnd (Y) \to M \in Bnd (X))$
6	5	3adant2	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F^{-1} \in (N Ismty M)) \to (N \in Bnd (Y) \to M \in Bnd (X))$
7	4 6	syld3an3	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to (N \in Bnd (Y) \to M \in Bnd (X))$
8	2 7	impbid	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to (M \in Bnd (X) \leftrightarrow N \in Bnd (Y))$

Metamath Proof Explorer