| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elex 3500 | . . . 4
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) | 
| 2 |  | elex 3500 | . . . 4
⊢ (𝐻 ∈ 𝑊 → 𝐻 ∈ V) | 
| 3 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) | 
| 4 |  | isismt.b | . . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) | 
| 5 | 3, 4 | eqtr4di 2794 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) | 
| 6 | 5 | f1oeq2d 6843 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ↔ 𝑓:𝐵–1-1-onto→(Base‘ℎ))) | 
| 7 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺)) | 
| 8 |  | isismt.d | . . . . . . . . . . . 12
⊢ 𝐷 = (dist‘𝐺) | 
| 9 | 7, 8 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = 𝐷) | 
| 10 | 9 | oveqd 7449 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑎(dist‘𝑔)𝑏) = (𝑎𝐷𝑏)) | 
| 11 | 10 | eqeq2d 2747 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → (((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) | 
| 12 | 5, 11 | raleqbidv 3345 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) | 
| 13 | 5, 12 | raleqbidv 3345 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) | 
| 14 | 6, 13 | anbi12d 632 | . . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏)) ↔ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏)))) | 
| 15 | 14 | abbidv 2807 | . . . . 5
⊢ (𝑔 = 𝐺 → {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))} = {𝑓 ∣ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))}) | 
| 16 |  | fveq2 6905 | . . . . . . . . 9
⊢ (ℎ = 𝐻 → (Base‘ℎ) = (Base‘𝐻)) | 
| 17 |  | isismt.p | . . . . . . . . 9
⊢ 𝑃 = (Base‘𝐻) | 
| 18 | 16, 17 | eqtr4di 2794 | . . . . . . . 8
⊢ (ℎ = 𝐻 → (Base‘ℎ) = 𝑃) | 
| 19 | 18 | f1oeq3d 6844 | . . . . . . 7
⊢ (ℎ = 𝐻 → (𝑓:𝐵–1-1-onto→(Base‘ℎ) ↔ 𝑓:𝐵–1-1-onto→𝑃)) | 
| 20 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (ℎ = 𝐻 → (dist‘ℎ) = (dist‘𝐻)) | 
| 21 |  | isismt.m | . . . . . . . . . . 11
⊢  − =
(dist‘𝐻) | 
| 22 | 20, 21 | eqtr4di 2794 | . . . . . . . . . 10
⊢ (ℎ = 𝐻 → (dist‘ℎ) = − ) | 
| 23 | 22 | oveqd 7449 | . . . . . . . . 9
⊢ (ℎ = 𝐻 → ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = ((𝑓‘𝑎) − (𝑓‘𝑏))) | 
| 24 | 23 | eqeq1d 2738 | . . . . . . . 8
⊢ (ℎ = 𝐻 → (((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))) | 
| 25 | 24 | 2ralbidv 3220 | . . . . . . 7
⊢ (ℎ = 𝐻 → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))) | 
| 26 | 19, 25 | anbi12d 632 | . . . . . 6
⊢ (ℎ = 𝐻 → ((𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏)) ↔ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)))) | 
| 27 | 26 | abbidv 2807 | . . . . 5
⊢ (ℎ = 𝐻 → {𝑓 ∣ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))} = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) | 
| 28 |  | df-ismt 28542 | . . . . 5
⊢ Ismt =
(𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))}) | 
| 29 |  | ovex 7465 | . . . . . 6
⊢ (𝑃 ↑m 𝐵) ∈ V | 
| 30 |  | f1of 6847 | . . . . . . . . 9
⊢ (𝑓:𝐵–1-1-onto→𝑃 → 𝑓:𝐵⟶𝑃) | 
| 31 | 17 | fvexi 6919 | . . . . . . . . . 10
⊢ 𝑃 ∈ V | 
| 32 | 4 | fvexi 6919 | . . . . . . . . . 10
⊢ 𝐵 ∈ V | 
| 33 | 31, 32 | elmap 8912 | . . . . . . . . 9
⊢ (𝑓 ∈ (𝑃 ↑m 𝐵) ↔ 𝑓:𝐵⟶𝑃) | 
| 34 | 30, 33 | sylibr 234 | . . . . . . . 8
⊢ (𝑓:𝐵–1-1-onto→𝑃 → 𝑓 ∈ (𝑃 ↑m 𝐵)) | 
| 35 | 34 | adantr 480 | . . . . . . 7
⊢ ((𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)) → 𝑓 ∈ (𝑃 ↑m 𝐵)) | 
| 36 | 35 | abssi 4069 | . . . . . 6
⊢ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ⊆ (𝑃 ↑m 𝐵) | 
| 37 | 29, 36 | ssexi 5321 | . . . . 5
⊢ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ∈ V | 
| 38 | 15, 27, 28, 37 | ovmpo 7594 | . . . 4
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V) → (𝐺Ismt𝐻) = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) | 
| 39 | 1, 2, 38 | syl2an 596 | . . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐺Ismt𝐻) = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) | 
| 40 | 39 | eleq2d 2826 | . 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))})) | 
| 41 |  | f1of 6847 | . . . . 5
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃) | 
| 42 |  | fex 7247 | . . . . 5
⊢ ((𝐹:𝐵⟶𝑃 ∧ 𝐵 ∈ V) → 𝐹 ∈ V) | 
| 43 | 41, 32, 42 | sylancl 586 | . . . 4
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹 ∈ V) | 
| 44 | 43 | adantr 480 | . . 3
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)) → 𝐹 ∈ V) | 
| 45 |  | f1oeq1 6835 | . . . 4
⊢ (𝑓 = 𝐹 → (𝑓:𝐵–1-1-onto→𝑃 ↔ 𝐹:𝐵–1-1-onto→𝑃)) | 
| 46 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑎) = (𝐹‘𝑎)) | 
| 47 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑏) = (𝐹‘𝑏)) | 
| 48 | 46, 47 | oveq12d 7450 | . . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑎) − (𝑓‘𝑏)) = ((𝐹‘𝑎) − (𝐹‘𝑏))) | 
| 49 | 48 | eqeq1d 2738 | . . . . 5
⊢ (𝑓 = 𝐹 → (((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) | 
| 50 | 49 | 2ralbidv 3220 | . . . 4
⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) | 
| 51 | 45, 50 | anbi12d 632 | . . 3
⊢ (𝑓 = 𝐹 → ((𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) | 
| 52 | 44, 51 | elab3 3685 | . 2
⊢ (𝐹 ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) | 
| 53 | 40, 52 | bitrdi 287 | 1
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) |