| Step | Hyp | Ref
| Expression |
| 1 | | uncfval.g |
. 2
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF
𝐺) |
| 2 | | df-uncf 18260 |
. . . 4
⊢
uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2))
∘func ((𝑓 ∘func ((𝑐‘0)
1stF (𝑐‘1))) 〈,〉F
((𝑐‘0)
2ndF (𝑐‘1))))) |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → uncurryF
= (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1)
evalF (𝑐‘2)) ∘func
((𝑓
∘func ((𝑐‘0) 1stF
(𝑐‘1)))
〈,〉F ((𝑐‘0) 2ndF
(𝑐‘1)))))) |
| 4 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → 𝑐 = 〈“𝐶𝐷𝐸”〉) |
| 5 | 4 | fveq1d 6908 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (𝑐‘1) = (〈“𝐶𝐷𝐸”〉‘1)) |
| 6 | | uncfval.c |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 7 | | s3fv1 14931 |
. . . . . . . 8
⊢ (𝐷 ∈ Cat →
(〈“𝐶𝐷𝐸”〉‘1) = 𝐷) |
| 8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (〈“𝐶𝐷𝐸”〉‘1) = 𝐷) |
| 9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (〈“𝐶𝐷𝐸”〉‘1) = 𝐷) |
| 10 | 5, 9 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (𝑐‘1) = 𝐷) |
| 11 | 4 | fveq1d 6908 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (𝑐‘2) = (〈“𝐶𝐷𝐸”〉‘2)) |
| 12 | | uncfval.d |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ Cat) |
| 13 | | s3fv2 14932 |
. . . . . . . 8
⊢ (𝐸 ∈ Cat →
(〈“𝐶𝐷𝐸”〉‘2) = 𝐸) |
| 14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (〈“𝐶𝐷𝐸”〉‘2) = 𝐸) |
| 15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (〈“𝐶𝐷𝐸”〉‘2) = 𝐸) |
| 16 | 11, 15 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (𝑐‘2) = 𝐸) |
| 17 | 10, 16 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → ((𝑐‘1) evalF (𝑐‘2)) = (𝐷 evalF 𝐸)) |
| 18 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → 𝑓 = 𝐺) |
| 19 | 4 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (𝑐‘0) = (〈“𝐶𝐷𝐸”〉‘0)) |
| 20 | | uncfval.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) |
| 21 | | funcrcl 17908 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)) → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
| 23 | 22 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 24 | | s3fv0 14930 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Cat →
(〈“𝐶𝐷𝐸”〉‘0) = 𝐶) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (〈“𝐶𝐷𝐸”〉‘0) = 𝐶) |
| 26 | 25 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (〈“𝐶𝐷𝐸”〉‘0) = 𝐶) |
| 27 | 19, 26 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (𝑐‘0) = 𝐶) |
| 28 | 27, 10 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → ((𝑐‘0) 1stF
(𝑐‘1)) = (𝐶
1stF 𝐷)) |
| 29 | 18, 28 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (𝑓 ∘func ((𝑐‘0)
1stF (𝑐‘1))) = (𝐺 ∘func (𝐶
1stF 𝐷))) |
| 30 | 27, 10 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → ((𝑐‘0) 2ndF
(𝑐‘1)) = (𝐶
2ndF 𝐷)) |
| 31 | 29, 30 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → ((𝑓 ∘func ((𝑐‘0)
1stF (𝑐‘1))) 〈,〉F
((𝑐‘0)
2ndF (𝑐‘1))) = ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))) |
| 32 | 17, 31 | oveq12d 7449 |
. . 3
⊢ ((𝜑 ∧ (𝑐 = 〈“𝐶𝐷𝐸”〉 ∧ 𝑓 = 𝐺)) → (((𝑐‘1) evalF (𝑐‘2))
∘func ((𝑓 ∘func ((𝑐‘0)
1stF (𝑐‘1))) 〈,〉F
((𝑐‘0)
2ndF (𝑐‘1)))) = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))) |
| 33 | | s3cli 14920 |
. . . 4
⊢
〈“𝐶𝐷𝐸”〉 ∈ Word V |
| 34 | | elex 3501 |
. . . 4
⊢
(〈“𝐶𝐷𝐸”〉 ∈ Word V →
〈“𝐶𝐷𝐸”〉 ∈ V) |
| 35 | 33, 34 | mp1i 13 |
. . 3
⊢ (𝜑 → 〈“𝐶𝐷𝐸”〉 ∈ V) |
| 36 | 20 | elexd 3504 |
. . 3
⊢ (𝜑 → 𝐺 ∈ V) |
| 37 | | ovexd 7466 |
. . 3
⊢ (𝜑 → ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))) ∈ V) |
| 38 | 3, 32, 35, 36, 37 | ovmpod 7585 |
. 2
⊢ (𝜑 → (〈“𝐶𝐷𝐸”〉 uncurryF
𝐺) = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))) |
| 39 | 1, 38 | eqtrid 2789 |
1
⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))) |