| 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 2737 |
. . . . 5
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 9 | | eqid 2737 |
. . . . 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 18268 |
. . . 4
⊢ (𝜑 → 𝐺 = 〈(𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))〉) |
| 13 | 3 | fvexi 6920 |
. . . . . 6
⊢ 𝐴 ∈ V |
| 14 | 13 | mptex 7243 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉) ∈ V |
| 15 | 13, 13 | mpoex 8104 |
. . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))))) ∈ V |
| 16 | 14, 15 | op2ndd 8025 |
. . . 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 7464 |
. . . . . 6
⊢ (𝑥𝐻𝑦) ∈ V |
| 22 | 21 | mptex 7243 |
. . . . 5
⊢ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) ∈ V |
| 23 | 22 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) ∈ V) |
| 24 | | curf2.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝐾 ∈ (𝑋𝐻𝑌)) |
| 26 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑥 = 𝑋) |
| 27 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑦 = 𝑌) |
| 28 | 26, 27 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌)) |
| 29 | 25, 28 | eleqtrrd 2844 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝐾 ∈ (𝑥𝐻𝑦)) |
| 30 | 7 | fvexi 6920 |
. . . . . . 7
⊢ 𝐵 ∈ V |
| 31 | 30 | mptex 7243 |
. . . . . 6
⊢ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) ∈ V |
| 32 | 31 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) ∈ V) |
| 33 | | simplrl 777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑥 = 𝑋) |
| 34 | 33 | opeq1d 4879 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 〈𝑥, 𝑧〉 = 〈𝑋, 𝑧〉) |
| 35 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑦 = 𝑌) |
| 36 | 35 | opeq1d 4879 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 〈𝑦, 𝑧〉 = 〈𝑌, 𝑧〉) |
| 37 | 34, 36 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉) = (〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)) |
| 38 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑔 = 𝐾) |
| 39 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝐼‘𝑧) = (𝐼‘𝑧)) |
| 40 | 37, 38, 39 | oveq123d 7452 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)) = (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))) |
| 41 | 40 | mpteq2dv 5244 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |
| 42 | 29, 32, 41 | fvmptdv2 7034 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ((𝑋(2nd ‘𝐺)𝑌) = (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))) → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))))) |
| 43 | 18, 20, 23, 42 | ovmpodv 7590 |
. . 3
⊢ (𝜑 → ((2nd
‘𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧))))) → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))))) |
| 44 | 17, 43 | mpd 15 |
. 2
⊢ (𝜑 → ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |
| 45 | 1, 44 | eqtrid 2789 |
1
⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |