Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. . . 4
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
2 | | elex 3185 |
. . . 4
⊢ (𝐻 ∈ 𝑊 → 𝐻 ∈ V) |
3 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → 𝑓 = 𝑓) |
4 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
5 | | isismt.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
6 | 4, 5 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) |
7 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘ℎ) = (Base‘ℎ)) |
8 | 3, 6, 7 | f1oeq123d 6046 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ↔ 𝑓:𝐵–1-1-onto→(Base‘ℎ))) |
9 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺)) |
10 | | isismt.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (dist‘𝐺) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = 𝐷) |
12 | 11 | oveqd 6566 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑎(dist‘𝑔)𝑏) = (𝑎𝐷𝑏)) |
13 | 12 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
14 | 6, 13 | raleqbidv 3129 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
15 | 6, 14 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
16 | 8, 15 | anbi12d 743 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏)) ↔ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏)))) |
17 | 16 | abbidv 2728 |
. . . . 5
⊢ (𝑔 = 𝐺 → {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))} = {𝑓 ∣ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))}) |
18 | | eqidd 2611 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → 𝑓 = 𝑓) |
19 | | eqidd 2611 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → 𝐵 = 𝐵) |
20 | | fveq2 6103 |
. . . . . . . . 9
⊢ (ℎ = 𝐻 → (Base‘ℎ) = (Base‘𝐻)) |
21 | | isismt.p |
. . . . . . . . 9
⊢ 𝑃 = (Base‘𝐻) |
22 | 20, 21 | syl6eqr 2662 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → (Base‘ℎ) = 𝑃) |
23 | 18, 19, 22 | f1oeq123d 6046 |
. . . . . . 7
⊢ (ℎ = 𝐻 → (𝑓:𝐵–1-1-onto→(Base‘ℎ) ↔ 𝑓:𝐵–1-1-onto→𝑃)) |
24 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (ℎ = 𝐻 → (dist‘ℎ) = (dist‘𝐻)) |
25 | | isismt.m |
. . . . . . . . . . 11
⊢ − =
(dist‘𝐻) |
26 | 24, 25 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (ℎ = 𝐻 → (dist‘ℎ) = − ) |
27 | 26 | oveqd 6566 |
. . . . . . . . 9
⊢ (ℎ = 𝐻 → ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = ((𝑓‘𝑎) − (𝑓‘𝑏))) |
28 | 27 | eqeq1d 2612 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → (((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
29 | 28 | 2ralbidv 2972 |
. . . . . . 7
⊢ (ℎ = 𝐻 → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))) |
30 | 23, 29 | anbi12d 743 |
. . . . . 6
⊢ (ℎ = 𝐻 → ((𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏)) ↔ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)))) |
31 | 30 | abbidv 2728 |
. . . . 5
⊢ (ℎ = 𝐻 → {𝑓 ∣ (𝑓:𝐵–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎𝐷𝑏))} = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) |
32 | | df-ismt 25228 |
. . . . 5
⊢ Ismt =
(𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))}) |
33 | | ovex 6577 |
. . . . . 6
⊢ (𝑃 ↑𝑚
𝐵) ∈
V |
34 | | f1of 6050 |
. . . . . . . . 9
⊢ (𝑓:𝐵–1-1-onto→𝑃 → 𝑓:𝐵⟶𝑃) |
35 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(Base‘𝐻)
∈ V |
36 | 21, 35 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝑃 ∈ V |
37 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(Base‘𝐺)
∈ V |
38 | 5, 37 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
39 | 36, 38 | elmap 7772 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑃 ↑𝑚 𝐵) ↔ 𝑓:𝐵⟶𝑃) |
40 | 34, 39 | sylibr 223 |
. . . . . . . 8
⊢ (𝑓:𝐵–1-1-onto→𝑃 → 𝑓 ∈ (𝑃 ↑𝑚 𝐵)) |
41 | 40 | adantr 480 |
. . . . . . 7
⊢ ((𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)) → 𝑓 ∈ (𝑃 ↑𝑚 𝐵)) |
42 | 41 | abssi 3640 |
. . . . . 6
⊢ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ⊆ (𝑃 ↑𝑚 𝐵) |
43 | 33, 42 | ssexi 4731 |
. . . . 5
⊢ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ∈ V |
44 | 17, 31, 32, 43 | ovmpt2 6694 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V) → (𝐺Ismt𝐻) = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) |
45 | 1, 2, 44 | syl2an 493 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐺Ismt𝐻) = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))}) |
46 | 45 | eleq2d 2673 |
. 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))})) |
47 | | f1of 6050 |
. . . . 5
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃) |
48 | | fex 6394 |
. . . . 5
⊢ ((𝐹:𝐵⟶𝑃 ∧ 𝐵 ∈ V) → 𝐹 ∈ V) |
49 | 47, 38, 48 | sylancl 693 |
. . . 4
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹 ∈ V) |
50 | 49 | adantr 480 |
. . 3
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)) → 𝐹 ∈ V) |
51 | | f1oeq1 6040 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝑓:𝐵–1-1-onto→𝑃 ↔ 𝐹:𝐵–1-1-onto→𝑃)) |
52 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑎) = (𝐹‘𝑎)) |
53 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑏) = (𝐹‘𝑏)) |
54 | 52, 53 | oveq12d 6567 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑎) − (𝑓‘𝑏)) = ((𝐹‘𝑎) − (𝐹‘𝑏))) |
55 | 54 | eqeq1d 2612 |
. . . . 5
⊢ (𝑓 = 𝐹 → (((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) |
56 | 55 | 2ralbidv 2972 |
. . . 4
⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) |
57 | 51, 56 | anbi12d 743 |
. . 3
⊢ (𝑓 = 𝐹 → ((𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏)) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) |
58 | 50, 57 | elab3 3327 |
. 2
⊢ (𝐹 ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑓‘𝑎) − (𝑓‘𝑏)) = (𝑎𝐷𝑏))} ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))) |
59 | 46, 58 | syl6bb 275 |
1
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) |