Metamath Proof Explorer


Theorem ismtybndlem

Description: Lemma for ismtybnd . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 19-Jan-2014)

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

Proof

Step Hyp Ref Expression
1 isismty ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋1-1-onto𝑌 ∧ ∀ 𝑧𝑋𝑤𝑋 ( 𝑧 𝑀 𝑤 ) = ( ( 𝐹𝑧 ) 𝑁 ( 𝐹𝑤 ) ) ) ) )
2 1 biimp3a ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝐹 : 𝑋1-1-onto𝑌 ∧ ∀ 𝑧𝑋𝑤𝑋 ( 𝑧 𝑀 𝑤 ) = ( ( 𝐹𝑧 ) 𝑁 ( 𝐹𝑤 ) ) ) )
3 2 simpld ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝐹 : 𝑋1-1-onto𝑌 )
4 f1ocnv ( 𝐹 : 𝑋1-1-onto𝑌 𝐹 : 𝑌1-1-onto𝑋 )
5 f1of ( 𝐹 : 𝑌1-1-onto𝑋 𝐹 : 𝑌𝑋 )
6 3 4 5 3syl ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝐹 : 𝑌𝑋 )
7 6 ffvelrnda ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ 𝑦𝑌 ) → ( 𝐹𝑦 ) ∈ 𝑋 )
8 oveq1 ( 𝑥 = ( 𝐹𝑦 ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) )
9 8 eqeq2d ( 𝑥 = ( 𝐹𝑦 ) → ( 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ↔ 𝑋 = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) )
10 9 rexbidv ( 𝑥 = ( 𝐹𝑦 ) → ( ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ↔ ∃ 𝑟 ∈ ℝ+ 𝑋 = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) )
11 10 rspcv ( ( 𝐹𝑦 ) ∈ 𝑋 → ( ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) )
12 7 11 syl ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ 𝑦𝑌 ) → ( ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑟 ∈ ℝ+ 𝑋 = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) )
13 imaeq2 ( 𝑋 = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) → ( 𝐹𝑋 ) = ( 𝐹 “ ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) )
14 f1ofo ( 𝐹 : 𝑋1-1-onto𝑌𝐹 : 𝑋onto𝑌 )
15 foima ( 𝐹 : 𝑋onto𝑌 → ( 𝐹𝑋 ) = 𝑌 )
16 3 14 15 3syl ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝐹𝑋 ) = 𝑌 )
17 16 adantr ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝐹𝑋 ) = 𝑌 )
18 rpxr ( 𝑟 ∈ ℝ+𝑟 ∈ ℝ* )
19 18 adantl ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ* )
20 7 19 anim12dan ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( ( 𝐹𝑦 ) ∈ 𝑋𝑟 ∈ ℝ* ) )
21 ismtyima ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( ( 𝐹𝑦 ) ∈ 𝑋𝑟 ∈ ℝ* ) ) → ( 𝐹 “ ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) = ( ( 𝐹 ‘ ( 𝐹𝑦 ) ) ( ball ‘ 𝑁 ) 𝑟 ) )
22 20 21 syldan ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝐹 “ ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) = ( ( 𝐹 ‘ ( 𝐹𝑦 ) ) ( ball ‘ 𝑁 ) 𝑟 ) )
23 simpl ( ( 𝑦𝑌𝑟 ∈ ℝ+ ) → 𝑦𝑌 )
24 f1ocnvfv2 ( ( 𝐹 : 𝑋1-1-onto𝑌𝑦𝑌 ) → ( 𝐹 ‘ ( 𝐹𝑦 ) ) = 𝑦 )
25 3 23 24 syl2an ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝐹 ‘ ( 𝐹𝑦 ) ) = 𝑦 )
26 25 oveq1d ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( ( 𝐹 ‘ ( 𝐹𝑦 ) ) ( ball ‘ 𝑁 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) )
27 22 26 eqtrd ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝐹 “ ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) )
28 17 27 eqeq12d ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( ( 𝐹𝑋 ) = ( 𝐹 “ ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) ) ↔ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
29 13 28 syl5ib ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑦𝑌𝑟 ∈ ℝ+ ) ) → ( 𝑋 = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) → 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
30 29 anassrs ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ 𝑦𝑌 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑋 = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) → 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
31 30 reximdva ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ 𝑦𝑌 ) → ( ∃ 𝑟 ∈ ℝ+ 𝑋 = ( ( 𝐹𝑦 ) ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
32 12 31 syld ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ 𝑦𝑌 ) → ( ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∃ 𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
33 32 ralrimdva ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∀ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
34 simp2 ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
35 33 34 jctild ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∀ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) ) )
36 35 3expib ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∀ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) ) ) )
37 36 com12 ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∀ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) ) ) )
38 37 impd ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∀ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) ) )
39 isbndx ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥𝑋𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
40 isbndx ( 𝑁 ∈ ( Bnd ‘ 𝑌 ) ↔ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ∀ 𝑦𝑌𝑟 ∈ ℝ+ 𝑌 = ( 𝑦 ( ball ‘ 𝑁 ) 𝑟 ) ) )
41 38 39 40 3imtr4g ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → 𝑁 ∈ ( Bnd ‘ 𝑌 ) ) )