Step | Hyp | Ref
| Expression |
1 | | elex 3414 |
. . . 4
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
2 | | elex 3414 |
. . . 4
⊢ (𝐻 ∈ 𝑊 → 𝐻 ∈ V) |
3 | | fveq2 6448 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
4 | | isismt.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
5 | 3, 4 | syl6eqr 2832 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) |
6 | 5 | f1oeq2d 6389 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ↔ 𝑓:𝐵–1-1-onto→(Base‘ℎ))) |
7 | | fveq2 6448 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺)) |
8 | | isismt.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (dist‘𝐺) |
9 | 7, 8 | syl6eqr 2832 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = 𝐷) |
10 | 9 | oveqd 6941 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑎(dist‘𝑔)𝑏) = (𝑎𝐷𝑏)) |
11 | 10 | eqeq2d 2788 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
12 | 5, 11 | raleqbidv 3326 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
13 | 5, 12 | raleqbidv 3326 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
14 | 6, 13 | anbi12d 624 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏)) ↔ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏)))) |
15 | 14 | abbidv 2906 |
. . . . 5
⊢ (𝑔 = 𝐺 → {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))} = {𝑓 ∣ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))}) |
16 | | eqidd 2779 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → 𝑓 = 𝑓) |
17 | | eqidd 2779 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → 𝐵 = 𝐵) |
18 | | fveq2 6448 |
. . . . . . . . 9
⊢ (ℎ = 𝐻 → (Base‘ℎ) = (Base‘𝐻)) |
19 | | isismt.p |
. . . . . . . . 9
⊢ 𝑃 = (Base‘𝐻) |
20 | 18, 19 | syl6eqr 2832 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → (Base‘ℎ) = 𝑃) |
21 | 16, 17, 20 | f1oeq123d 6388 |
. . . . . . 7
⊢ (ℎ = 𝐻 → (𝑓:𝐵–1-1-onto→(Base‘ℎ) ↔ 𝑓:𝐵–1-1-onto→𝑃)) |
22 | | fveq2 6448 |
. . . . . . . . . . 11
⊢ (ℎ = 𝐻 → (dist‘ℎ) = (dist‘𝐻)) |
23 | | isismt.m |
. . . . . . . . . . 11
⊢ − =
(dist‘𝐻) |
24 | 22, 23 | syl6eqr 2832 |
. . . . . . . . . 10
⊢ (ℎ = 𝐻 → (dist‘ℎ) = − ) |
25 | 24 | oveqd 6941 |
. . . . . . . . 9
⊢ (ℎ = 𝐻 → ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = ((𝑓‘𝑎) − (𝑓‘𝑏))) |
26 | 25 | eqeq1d 2780 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → (((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
27 | 26 | 2ralbidv 3171 |
. . . . . . 7
⊢ (ℎ = 𝐻 → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
28 | 21, 27 | anbi12d 624 |
. . . . . 6
⊢ (ℎ = 𝐻 → ((𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏)) ↔ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)))) |
29 | 28 | abbidv 2906 |
. . . . 5
⊢ (ℎ = 𝐻 → {𝑓 ∣ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))} = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) |
30 | | df-ismt 25888 |
. . . . 5
⊢ Ismt =
(𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))}) |
31 | | ovex 6956 |
. . . . . 6
⊢ (𝑃 ↑𝑚
𝐵) ∈
V |
32 | | f1of 6393 |
. . . . . . . . 9
⊢ (𝑓:𝐵–1-1-onto→𝑃 → 𝑓:𝐵⟶𝑃) |
33 | 19 | fvexi 6462 |
. . . . . . . . . 10
⊢ 𝑃 ∈ V |
34 | 4 | fvexi 6462 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
35 | 33, 34 | elmap 8171 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑃 ↑𝑚 𝐵) ↔ 𝑓:𝐵⟶𝑃) |
36 | 32, 35 | sylibr 226 |
. . . . . . . 8
⊢ (𝑓:𝐵–1-1-onto→𝑃 → 𝑓 ∈ (𝑃 ↑𝑚 𝐵)) |
37 | 36 | adantr 474 |
. . . . . . 7
⊢ ((𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)) → 𝑓 ∈ (𝑃 ↑𝑚 𝐵)) |
38 | 37 | abssi 3898 |
. . . . . 6
⊢ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ⊆ (𝑃 ↑𝑚 𝐵) |
39 | 31, 38 | ssexi 5042 |
. . . . 5
⊢ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ∈ V |
40 | 15, 29, 30, 39 | ovmpt2 7075 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V) → (𝐺Ismt𝐻) = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) |
41 | 1, 2, 40 | syl2an 589 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐺Ismt𝐻) = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) |
42 | 41 | eleq2d 2845 |
. 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))})) |
43 | | f1of 6393 |
. . . . 5
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃) |
44 | | fex 6763 |
. . . . 5
⊢ ((𝐹:𝐵⟶𝑃 ∧ 𝐵 ∈ V) → 𝐹 ∈ V) |
45 | 43, 34, 44 | sylancl 580 |
. . . 4
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹 ∈ V) |
46 | 45 | adantr 474 |
. . 3
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)) → 𝐹 ∈ V) |
47 | | f1oeq1 6382 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝑓:𝐵–1-1-onto→𝑃 ↔ 𝐹:𝐵–1-1-onto→𝑃)) |
48 | | fveq1 6447 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑎) = (𝐹‘𝑎)) |
49 | | fveq1 6447 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑏) = (𝐹‘𝑏)) |
50 | 48, 49 | oveq12d 6942 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑎) − (𝑓‘𝑏)) = ((𝐹‘𝑎) − (𝐹‘𝑏))) |
51 | 50 | eqeq1d 2780 |
. . . . 5
⊢ (𝑓 = 𝐹 → (((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) |
52 | 51 | 2ralbidv 3171 |
. . . 4
⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) |
53 | 47, 52 | anbi12d 624 |
. . 3
⊢ (𝑓 = 𝐹 → ((𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) |
54 | 46, 53 | elab3 3566 |
. 2
⊢ (𝐹 ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) |
55 | 42, 54 | syl6bb 279 |
1
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) |