Metamath Proof Explorer

Theorem ismtybnd

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

Ref Expression
Assertion ismtybnd ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y ∧ F ∈ M Ismty N → M ∈ Bnd ⁡ X ↔ N ∈ Bnd ⁡ Y

Proof

Step Hyp Ref Expression
1 ismtybndlem ⊢ N ∈ ∞Met ⁡ Y ∧ F ∈ M Ismty N → M ∈ Bnd ⁡ X → N ∈ Bnd ⁡ Y
2 1 3adant1 ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y ∧ F ∈ M Ismty N → M ∈ Bnd ⁡ X → N ∈ Bnd ⁡ Y
3 ismtycnv ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y → F ∈ M Ismty N → F -1 ∈ N Ismty M
4 3 3impia ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y ∧ F ∈ M Ismty N → F -1 ∈ N Ismty M
5 ismtybndlem ⊢ M ∈ ∞Met ⁡ X ∧ F -1 ∈ N Ismty M → N ∈ Bnd ⁡ Y → M ∈ Bnd ⁡ X
6 5 3adant2 ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y ∧ F -1 ∈ N Ismty M → N ∈ Bnd ⁡ Y → M ∈ Bnd ⁡ X
7 4 6 syld3an3 ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y ∧ F ∈ M Ismty N → N ∈ Bnd ⁡ Y → M ∈ Bnd ⁡ X
8 2 7 impbid ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y ∧ F ∈ M Ismty N → M ∈ Bnd ⁡ X ↔ N ∈ Bnd ⁡ Y