Definition df-uncf 17459

Description: Define the uncurry functor, which can be defined equationally using eval_F. Strictly speaking, the third category argument is not needed, since the resulting functor is extensionally equal regardless, but it is used in the equational definition and is too much work to remove. (Contributed by Mario Carneiro, 13-Jan-2017.)

Assertion

Ref	Expression
df-uncf	⊢ uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))

Distinct variable group:   𝑓,𝑐

Detailed syntax breakdown of Definition df-uncf

Step	Hyp	Ref	Expression
1		cuncf 17455	. 2 class uncurryF
2		vc	. . 3 setvar 𝑐
3		vf	. . 3 setvar 𝑓
4		cvv 3495	. . 3 class V
5		c1 10532	. . . . . 6 class 1
6	2	cv 1532	. . . . . 6 class 𝑐
7	5, 6	cfv 6350	. . . . 5 class (𝑐‘1)
8		c2 11686	. . . . . 6 class 2
9	8, 6	cfv 6350	. . . . 5 class (𝑐‘2)
10		cevlf 17453	. . . . 5 class evalF
11	7, 9, 10	co 7150	. . . 4 class ((𝑐‘1) evalF (𝑐‘2))
12	3	cv 1532	. . . . . 6 class 𝑓
13		cc0 10531	. . . . . . . 8 class 0
14	13, 6	cfv 6350	. . . . . . 7 class (𝑐‘0)
15		c1stf 17413	. . . . . . 7 class 1stF
16	14, 7, 15	co 7150	. . . . . 6 class ((𝑐‘0) 1stF (𝑐‘1))
17		ccofu 17120	. . . . . 6 class ∘func
18	12, 16, 17	co 7150	. . . . 5 class (𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1)))
19		c2ndf 17414	. . . . . 6 class 2ndF
20	14, 7, 19	co 7150	. . . . 5 class ((𝑐‘0) 2ndF (𝑐‘1))
21		cprf 17415	. . . . 5 class ⟨,⟩F
22	18, 20, 21	co 7150	. . . 4 class ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))
23	11, 22, 17	co 7150	. . 3 class (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1))))
24	2, 3, 4, 4, 23	cmpo 7152	. 2 class (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))
25	1, 24	wceq 1533	1 wff uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))

This definition is referenced by:  uncfval  17478