Step | Hyp | Ref
| Expression |
1 | | curf2.l |
. 2
⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) |
2 | | curf2.g |
. . . . 5
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) |
3 | | curf2.a |
. . . . 5
⊢ 𝐴 = (Base‘𝐶) |
4 | | curf2.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
5 | | curf2.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ Cat) |
6 | | curf2.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
7 | | curf2.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐷) |
8 | | eqid 2733 |
. . . . 5
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
9 | | eqid 2733 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
10 | | curf2.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
11 | | curf2.i |
. . . . 5
⊢ 𝐼 = (Id‘𝐷) |
12 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | curfval 17969 |
. . . 4
⊢ (𝜑 → 𝐺 = 〈(𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))〉) |
13 | 3 | fvexi 6806 |
. . . . . 6
⊢ 𝐴 ∈ V |
14 | 13 | mptex 7119 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉) ∈ V |
15 | 13, 13 | mpoex 7940 |
. . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))))) ∈ V |
16 | 14, 15 | op2ndd 7862 |
. . . 4
⊢ (𝐺 = 〈(𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))〉 → (2nd
‘𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))) |
17 | 12, 16 | syl 17 |
. . 3
⊢ (𝜑 → (2nd
‘𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))) |
18 | | curf2.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
19 | | curf2.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
20 | 19 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑌 ∈ 𝐴) |
21 | | ovex 7328 |
. . . . . 6
⊢ (𝑥𝐻𝑦) ∈ V |
22 | 21 | mptex 7119 |
. . . . 5
⊢ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) ∈ V |
23 | 22 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) ∈ V) |
24 | | curf2.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) |
25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝐾 ∈ (𝑋𝐻𝑌)) |
26 | | simprl 767 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑥 = 𝑋) |
27 | | simprr 769 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑦 = 𝑌) |
28 | 26, 27 | oveq12d 7313 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌)) |
29 | 25, 28 | eleqtrrd 2837 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝐾 ∈ (𝑥𝐻𝑦)) |
30 | 7 | fvexi 6806 |
. . . . . . 7
⊢ 𝐵 ∈ V |
31 | 30 | mptex 7119 |
. . . . . 6
⊢ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) ∈ V |
32 | 31 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) ∈ V) |
33 | | simplrl 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑥 = 𝑋) |
34 | 33 | opeq1d 4812 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 〈𝑥, 𝑧〉 = 〈𝑋, 𝑧〉) |
35 | | simplrr 774 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑦 = 𝑌) |
36 | 35 | opeq1d 4812 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 〈𝑦, 𝑧〉 = 〈𝑌, 𝑧〉) |
37 | 34, 36 | oveq12d 7313 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉) = (〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)) |
38 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑔 = 𝐾) |
39 | | eqidd 2734 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝐼‘𝑧) = (𝐼‘𝑧)) |
40 | 37, 38, 39 | oveq123d 7316 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)) = (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))) |
41 | 40 | mpteq2dv 5179 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |
42 | 29, 32, 41 | fvmptdv2 6913 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ((𝑋(2nd ‘𝐺)𝑌) = (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))))) |
43 | 18, 20, 23, 42 | ovmpodv 7450 |
. . 3
⊢ (𝜑 → ((2nd
‘𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))))) → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))))) |
44 | 17, 43 | mpd 15 |
. 2
⊢ (𝜑 → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |
45 | 1, 44 | eqtrid 2785 |
1
⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |