Definition df-uncf 16678

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 16674	. 2 class uncurryF
2		vc	. . 3 setvar 𝑐
3		vf	. . 3 setvar 𝑓
4		cvv 3173	. . 3 class V
5		c1 9816	. . . . . 6 class 1
6	2	cv 1474	. . . . . 6 class 𝑐
7	5, 6	cfv 5804	. . . . 5 class (𝑐‘1)
8		c2 10947	. . . . . 6 class 2
9	8, 6	cfv 5804	. . . . 5 class (𝑐‘2)
10		cevlf 16672	. . . . 5 class evalF
11	7, 9, 10	co 6549	. . . 4 class ((𝑐‘1) evalF (𝑐‘2))
12	3	cv 1474	. . . . . 6 class 𝑓
13		cc0 9815	. . . . . . . 8 class 0
14	13, 6	cfv 5804	. . . . . . 7 class (𝑐‘0)
15		c1stf 16632	. . . . . . 7 class 1stF
16	14, 7, 15	co 6549	. . . . . 6 class ((𝑐‘0) 1stF (𝑐‘1))
17		ccofu 16339	. . . . . 6 class ∘func
18	12, 16, 17	co 6549	. . . . 5 class (𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1)))
19		c2ndf 16633	. . . . . 6 class 2ndF
20	14, 7, 19	co 6549	. . . . 5 class ((𝑐‘0) 2ndF (𝑐‘1))
21		cprf 16634	. . . . 5 class ⟨,⟩F
22	18, 20, 21	co 6549	. . . 4 class ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))
23	11, 22, 17	co 6549	. . 3 class (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1))))
24	2, 3, 4, 4, 23	cmpt2 6551	. 2 class (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))
25	1, 24	wceq 1475	1 wff uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))

This definition is referenced by:  uncfval  16697