| 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
|
ffvelcdmda |
⊢ ( ( ( 𝑀 ∈ ( ∞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
|
imbitrid |
⊢ ( ( ( 𝑀 ∈ ( ∞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 ‘ 𝑌 ) ) ) |