Theorem ismtybnd

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

	Ref	Expression
Assertion	ismtybnd	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ismtybndlem	⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) )
2	1	3adant1	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) )
3		ismtycnv	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) → ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ) )
4	3	3impia	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) )
5		ismtybndlem	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) → 𝑀 ∈ ( Bnd ‘ 𝑋 ) ) )
6	5	3adant2	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) → 𝑀 ∈ ( Bnd ‘ 𝑋 ) ) )
7	4 6	syld3an3	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) → 𝑀 ∈ ( Bnd ‘ 𝑋 ) ) )
8	2 7	impbid	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) )