Step | Hyp | Ref
| Expression |
1 | | curfpropd.1 |
. . . . 5
⊢ (𝜑 → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
2 | 1 | homfeqbas 17581 |
. . . 4
⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵)) |
3 | | curfpropd.3 |
. . . . . . . 8
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
4 | 3 | homfeqbas 17581 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
5 | 4 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (Base‘𝐶) = (Base‘𝐷)) |
6 | 5 | mpteq1d 5201 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)) = (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦))) |
7 | 5 | adantr 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷)) |
8 | | eqid 2733 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
9 | | eqid 2733 |
. . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
10 | | eqid 2733 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
11 | 3 | ad2antrr 725 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
12 | | simprl 770 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
13 | | simprr 772 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑧 ∈ (Base‘𝐶)) |
14 | 8, 9, 10, 11, 12, 13 | homfeqval 17582 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧)) |
15 | | curfpropd.2 |
. . . . . . . . . . 11
⊢ (𝜑 →
(compf‘𝐴) = (compf‘𝐵)) |
16 | | curfpropd.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ Cat) |
17 | | curfpropd.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ Cat) |
18 | 1, 15, 16, 17 | cidpropd 17595 |
. . . . . . . . . 10
⊢ (𝜑 → (Id‘𝐴) = (Id‘𝐵)) |
19 | 18 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (Id‘𝐴) = (Id‘𝐵)) |
20 | 19 | fveq1d 6845 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ((Id‘𝐴)‘𝑥) = ((Id‘𝐵)‘𝑥)) |
21 | 20 | oveq1d 7373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (((Id‘𝐴)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔) = (((Id‘𝐵)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)) |
22 | 14, 21 | mpteq12dv 5197 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔))) |
23 | 5, 7, 22 | mpoeq123dva 7432 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))) |
24 | 6, 23 | opeq12d 4839 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → ⟨(𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩ = ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩) |
25 | 2, 24 | mpteq12dva 5195 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐴) ↦ ⟨(𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩) = (𝑥 ∈ (Base‘𝐵) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩)) |
26 | 2 | adantr 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵)) |
27 | | eqid 2733 |
. . . . . 6
⊢
(Base‘𝐴) =
(Base‘𝐴) |
28 | | eqid 2733 |
. . . . . 6
⊢ (Hom
‘𝐴) = (Hom
‘𝐴) |
29 | | eqid 2733 |
. . . . . 6
⊢ (Hom
‘𝐵) = (Hom
‘𝐵) |
30 | 1 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
31 | | simprl 770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑥 ∈ (Base‘𝐴)) |
32 | | simprr 772 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑦 ∈ (Base‘𝐴)) |
33 | 27, 28, 29, 30, 31, 32 | homfeqval 17582 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑥(Hom ‘𝐴)𝑦) = (𝑥(Hom ‘𝐵)𝑦)) |
34 | 4 | ad2antrr 725 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (Base‘𝐶) = (Base‘𝐷)) |
35 | | curfpropd.4 |
. . . . . . . . . 10
⊢ (𝜑 →
(compf‘𝐶) = (compf‘𝐷)) |
36 | | curfpropd.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Cat) |
37 | | curfpropd.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ Cat) |
38 | 3, 35, 36, 37 | cidpropd 17595 |
. . . . . . . . 9
⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷)) |
39 | 38 | ad3antrrr 729 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑧 ∈ (Base‘𝐶)) → (Id‘𝐶) = (Id‘𝐷)) |
40 | 39 | fveq1d 6845 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑧 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑧) = ((Id‘𝐷)‘𝑧)) |
41 | 40 | oveq2d 7374 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐶)‘𝑧)) = (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) |
42 | 34, 41 | mpteq12dva 5195 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐶)‘𝑧))) = (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))) |
43 | 33, 42 | mpteq12dva 5195 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦) ↦ (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐶)‘𝑧)))) = (𝑔 ∈ (𝑥(Hom ‘𝐵)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))) |
44 | 2, 26, 43 | mpoeq123dva 7432 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐴), 𝑦 ∈ (Base‘𝐴) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦) ↦ (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐶)‘𝑧))))) = (𝑥 ∈ (Base‘𝐵), 𝑦 ∈ (Base‘𝐵) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐵)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))) |
45 | 25, 44 | opeq12d 4839 |
. 2
⊢ (𝜑 → ⟨(𝑥 ∈ (Base‘𝐴) ↦ ⟨(𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝐴), 𝑦 ∈ (Base‘𝐴) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦) ↦ (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐶)‘𝑧)))))⟩ = ⟨(𝑥 ∈ (Base‘𝐵) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝐵), 𝑦 ∈ (Base‘𝐵) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐵)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))⟩) |
46 | | eqid 2733 |
. . 3
⊢
(⟨𝐴, 𝐶⟩ curryF
𝐹) = (⟨𝐴, 𝐶⟩ curryF 𝐹) |
47 | | curfpropd.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ ((𝐴 ×c 𝐶) Func 𝐸)) |
48 | | eqid 2733 |
. . 3
⊢
(Id‘𝐴) =
(Id‘𝐴) |
49 | | eqid 2733 |
. . 3
⊢
(Id‘𝐶) =
(Id‘𝐶) |
50 | 46, 27, 16, 36, 47, 8, 9, 48, 28, 49 | curfval 18117 |
. 2
⊢ (𝜑 → (⟨𝐴, 𝐶⟩ curryF 𝐹) = ⟨(𝑥 ∈ (Base‘𝐴) ↦ ⟨(𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝐴), 𝑦 ∈ (Base‘𝐴) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦) ↦ (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐶)‘𝑧)))))⟩) |
51 | | eqid 2733 |
. . 3
⊢
(⟨𝐵, 𝐷⟩ curryF
𝐹) = (⟨𝐵, 𝐷⟩ curryF 𝐹) |
52 | | eqid 2733 |
. . 3
⊢
(Base‘𝐵) =
(Base‘𝐵) |
53 | 1, 15, 3, 35, 16, 17, 36, 37 | xpcpropd 18102 |
. . . . 5
⊢ (𝜑 → (𝐴 ×c 𝐶) = (𝐵 ×c 𝐷)) |
54 | 53 | oveq1d 7373 |
. . . 4
⊢ (𝜑 → ((𝐴 ×c 𝐶) Func 𝐸) = ((𝐵 ×c 𝐷) Func 𝐸)) |
55 | 47, 54 | eleqtrd 2836 |
. . 3
⊢ (𝜑 → 𝐹 ∈ ((𝐵 ×c 𝐷) Func 𝐸)) |
56 | | eqid 2733 |
. . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) |
57 | | eqid 2733 |
. . 3
⊢
(Id‘𝐵) =
(Id‘𝐵) |
58 | | eqid 2733 |
. . 3
⊢
(Id‘𝐷) =
(Id‘𝐷) |
59 | 51, 52, 17, 37, 55, 56, 10, 57, 29, 58 | curfval 18117 |
. 2
⊢ (𝜑 → (⟨𝐵, 𝐷⟩ curryF 𝐹) = ⟨(𝑥 ∈ (Base‘𝐵) ↦ ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝐵), 𝑦 ∈ (Base‘𝐵) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐵)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))⟩) |
60 | 45, 50, 59 | 3eqtr4d 2783 |
1
⊢ (𝜑 → (⟨𝐴, 𝐶⟩ curryF 𝐹) = (⟨𝐵, 𝐷⟩ curryF 𝐹)) |