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 2622 |
. . . . 5
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
9 | | eqid 2622 |
. . . . 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 16863 |
. . . 4
⊢ (𝜑 → 𝐺 = 〈(𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))〉) |
13 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
14 | 3, 13 | eqeltri 2697 |
. . . . . 6
⊢ 𝐴 ∈ V |
15 | 14 | mptex 6486 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉) ∈ V |
16 | 14, 14 | mpt2ex 7247 |
. . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))))) ∈ V |
17 | 15, 16 | op2ndd 7179 |
. . . 4
⊢ (𝐺 = 〈(𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))〉 → (2nd
‘𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))) |
18 | 12, 17 | syl 17 |
. . 3
⊢ (𝜑 → (2nd
‘𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))) |
19 | | curf2.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
20 | | curf2.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
21 | 20 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑌 ∈ 𝐴) |
22 | | ovex 6678 |
. . . . . 6
⊢ (𝑥𝐻𝑦) ∈ V |
23 | 22 | mptex 6486 |
. . . . 5
⊢ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) ∈ V |
24 | 23 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) ∈ V) |
25 | | curf2.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) |
26 | 25 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝐾 ∈ (𝑋𝐻𝑌)) |
27 | | simprl 794 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑥 = 𝑋) |
28 | | simprr 796 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑦 = 𝑌) |
29 | 27, 28 | oveq12d 6668 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌)) |
30 | 26, 29 | eleqtrrd 2704 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝐾 ∈ (𝑥𝐻𝑦)) |
31 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐷)
∈ V |
32 | 7, 31 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐵 ∈ V |
33 | 32 | mptex 6486 |
. . . . . 6
⊢ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) ∈ V |
34 | 33 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) ∈ V) |
35 | | simplrl 800 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑥 = 𝑋) |
36 | 35 | opeq1d 4408 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 〈𝑥, 𝑧〉 = 〈𝑋, 𝑧〉) |
37 | | simplrr 801 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑦 = 𝑌) |
38 | 37 | opeq1d 4408 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 〈𝑦, 𝑧〉 = 〈𝑌, 𝑧〉) |
39 | 36, 38 | oveq12d 6668 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉) = (〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)) |
40 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑔 = 𝐾) |
41 | | eqidd 2623 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝐼‘𝑧) = (𝐼‘𝑧)) |
42 | 39, 40, 41 | oveq123d 6671 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)) = (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))) |
43 | 42 | mpteq2dv 4745 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |
44 | 30, 34, 43 | fvmptdv2 6298 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ((𝑋(2nd ‘𝐺)𝑌) = (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))))) |
45 | 19, 21, 24, 44 | ovmpt2dv 6793 |
. . 3
⊢ (𝜑 → ((2nd
‘𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))))) → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))))) |
46 | 18, 45 | mpd 15 |
. 2
⊢ (𝜑 → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |
47 | 1, 46 | syl5eq 2668 |
1
⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |