| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | curf1.k | . 2
⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) | 
| 2 |  | curfval.g | . . . 4
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) | 
| 3 |  | curfval.a | . . . 4
⊢ 𝐴 = (Base‘𝐶) | 
| 4 |  | curfval.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 5 |  | curfval.d | . . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) | 
| 6 |  | curfval.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) | 
| 7 |  | curfval.b | . . . 4
⊢ 𝐵 = (Base‘𝐷) | 
| 8 |  | curf1.j | . . . 4
⊢ 𝐽 = (Hom ‘𝐷) | 
| 9 |  | curf1.1 | . . . 4
⊢  1 =
(Id‘𝐶) | 
| 10 | 2, 3, 4, 5, 6, 7, 8, 9 | curf1fval 18269 | . . 3
⊢ (𝜑 → (1st
‘𝐺) = (𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉)) | 
| 11 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) | 
| 12 | 11 | oveq1d 7446 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥(1st ‘𝐹)𝑦) = (𝑋(1st ‘𝐹)𝑦)) | 
| 13 | 12 | mpteq2dv 5244 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦))) | 
| 14 |  | simp1r 1199 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → 𝑥 = 𝑋) | 
| 15 | 14 | opeq1d 4879 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑦〉) | 
| 16 | 14 | opeq1d 4879 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → 〈𝑥, 𝑧〉 = 〈𝑋, 𝑧〉) | 
| 17 | 15, 16 | oveq12d 7449 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉) = (〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)) | 
| 18 | 14 | fveq2d 6910 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ( 1 ‘𝑥) = ( 1 ‘𝑋)) | 
| 19 |  | eqidd 2738 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → 𝑔 = 𝑔) | 
| 20 | 17, 18, 19 | oveq123d 7452 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔) = (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)) | 
| 21 | 20 | mpteq2dv 5244 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)) = (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) | 
| 22 | 21 | mpoeq3dva 7510 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔))) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))) | 
| 23 | 13, 22 | opeq12d 4881 | . . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉 = 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉) | 
| 24 |  | curf1.x | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝐴) | 
| 25 |  | opex 5469 | . . . 4
⊢
〈(𝑦 ∈
𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉 ∈ V | 
| 26 | 25 | a1i 11 | . . 3
⊢ (𝜑 → 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉 ∈ V) | 
| 27 | 10, 23, 24, 26 | fvmptd 7023 | . 2
⊢ (𝜑 → ((1st
‘𝐺)‘𝑋) = 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉) | 
| 28 | 1, 27 | eqtrid 2789 | 1
⊢ (𝜑 → 𝐾 = 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉) |