Step | Hyp | Ref
| Expression |
1 | | curfpropd.1 |
. . . . 5
⊢ (𝜑 → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
2 | 1 | homfeqbas 17386 |
. . . 4
⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵)) |
3 | | curfpropd.3 |
. . . . . . . 8
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
4 | 3 | homfeqbas 17386 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (Base‘𝐶) = (Base‘𝐷)) |
6 | 5 | mpteq1d 5173 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)) = (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦))) |
7 | 5 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷)) |
8 | | eqid 2739 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
9 | | eqid 2739 |
. . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
10 | | eqid 2739 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
11 | 3 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
12 | | simprl 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
13 | | simprr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑧 ∈ (Base‘𝐶)) |
14 | 8, 9, 10, 11, 12, 13 | homfeqval 17387 |
. . . . . . 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 17400 |
. . . . . . . . . 10
⊢ (𝜑 → (Id‘𝐴) = (Id‘𝐵)) |
19 | 18 | ad2antrr 722 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (Id‘𝐴) = (Id‘𝐵)) |
20 | 19 | fveq1d 6770 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ((Id‘𝐴)‘𝑥) = ((Id‘𝐵)‘𝑥)) |
21 | 20 | oveq1d 7283 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (((Id‘𝐴)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔) = (((Id‘𝐵)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)) |
22 | 14, 21 | mpteq12dv 5169 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔))) |
23 | 5, 7, 22 | mpoeq123dva 7340 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))) |
24 | 6, 23 | opeq12d 4817 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → 〈(𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉 = 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉) |
25 | 2, 24 | mpteq12dva 5167 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐴) ↦ 〈(𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉) = (𝑥 ∈ (Base‘𝐵) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉)) |
26 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵)) |
27 | | eqid 2739 |
. . . . . 6
⊢
(Base‘𝐴) =
(Base‘𝐴) |
28 | | eqid 2739 |
. . . . . 6
⊢ (Hom
‘𝐴) = (Hom
‘𝐴) |
29 | | eqid 2739 |
. . . . . 6
⊢ (Hom
‘𝐵) = (Hom
‘𝐵) |
30 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
31 | | simprl 767 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑥 ∈ (Base‘𝐴)) |
32 | | simprr 769 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑦 ∈ (Base‘𝐴)) |
33 | 27, 28, 29, 30, 31, 32 | homfeqval 17387 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑥(Hom ‘𝐴)𝑦) = (𝑥(Hom ‘𝐵)𝑦)) |
34 | 4 | ad2antrr 722 |
. . . . . 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 17400 |
. . . . . . . . 9
⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷)) |
39 | 38 | ad3antrrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑧 ∈ (Base‘𝐶)) → (Id‘𝐶) = (Id‘𝐷)) |
40 | 39 | fveq1d 6770 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑧 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑧) = ((Id‘𝐷)‘𝑧)) |
41 | 40 | oveq2d 7284 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐶)‘𝑧)) = (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))) |
42 | 34, 41 | mpteq12dva 5167 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐶)‘𝑧))) = (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))) |
43 | 33, 42 | mpteq12dva 5167 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦) ↦ (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐶)‘𝑧)))) = (𝑔 ∈ (𝑥(Hom ‘𝐵)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) |
44 | 2, 26, 43 | mpoeq123dva 7340 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐴), 𝑦 ∈ (Base‘𝐴) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦) ↦ (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐶)‘𝑧))))) = (𝑥 ∈ (Base‘𝐵), 𝑦 ∈ (Base‘𝐵) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐵)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))) |
45 | 25, 44 | opeq12d 4817 |
. 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 2739 |
. . 3
⊢
(〈𝐴, 𝐶〉 curryF
𝐹) = (〈𝐴, 𝐶〉 curryF 𝐹) |
47 | | curfpropd.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ ((𝐴 ×c 𝐶) Func 𝐸)) |
48 | | eqid 2739 |
. . 3
⊢
(Id‘𝐴) =
(Id‘𝐴) |
49 | | eqid 2739 |
. . 3
⊢
(Id‘𝐶) =
(Id‘𝐶) |
50 | 46, 27, 16, 36, 47, 8, 9, 48, 28, 49 | curfval 17922 |
. 2
⊢ (𝜑 → (〈𝐴, 𝐶〉 curryF 𝐹) = 〈(𝑥 ∈ (Base‘𝐴) ↦ 〈(𝑦 ∈ (Base‘𝐶) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐶), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((Id‘𝐴)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝐴), 𝑦 ∈ (Base‘𝐴) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐴)𝑦) ↦ (𝑧 ∈ (Base‘𝐶) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐶)‘𝑧)))))〉) |
51 | | eqid 2739 |
. . 3
⊢
(〈𝐵, 𝐷〉 curryF
𝐹) = (〈𝐵, 𝐷〉 curryF 𝐹) |
52 | | eqid 2739 |
. . 3
⊢
(Base‘𝐵) =
(Base‘𝐵) |
53 | 1, 15, 3, 35, 16, 17, 36, 37 | xpcpropd 17907 |
. . . . 5
⊢ (𝜑 → (𝐴 ×c 𝐶) = (𝐵 ×c 𝐷)) |
54 | 53 | oveq1d 7283 |
. . . 4
⊢ (𝜑 → ((𝐴 ×c 𝐶) Func 𝐸) = ((𝐵 ×c 𝐷) Func 𝐸)) |
55 | 47, 54 | eleqtrd 2842 |
. . 3
⊢ (𝜑 → 𝐹 ∈ ((𝐵 ×c 𝐷) Func 𝐸)) |
56 | | eqid 2739 |
. . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) |
57 | | eqid 2739 |
. . 3
⊢
(Id‘𝐵) =
(Id‘𝐵) |
58 | | eqid 2739 |
. . 3
⊢
(Id‘𝐷) =
(Id‘𝐷) |
59 | 51, 52, 17, 37, 55, 56, 10, 57, 29, 58 | curfval 17922 |
. 2
⊢ (𝜑 → (〈𝐵, 𝐷〉 curryF 𝐹) = 〈(𝑥 ∈ (Base‘𝐵) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐵)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝐵), 𝑦 ∈ (Base‘𝐵) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐵)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))〉) |
60 | 45, 50, 59 | 3eqtr4d 2789 |
1
⊢ (𝜑 → (〈𝐴, 𝐶〉 curryF 𝐹) = (〈𝐵, 𝐷〉 curryF 𝐹)) |