Definition df-uncf

Description: Define the uncurry functor, which can be defined equationally using evalF . 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)

	Ref	Expression
Assertion	df-uncf	|- uncurryF = ( c e. _V , f e. _V |-> ( ( ( c ` 1 ) evalF ( c ` 2 ) ) o.func ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuncf	|- uncurryF
1		vc	|- c
2		cvv	|- _V
3		vf	|- f
4	1	cv	|- c
5		c1	|- 1
6	5 4	cfv	|- ( c ` 1 )
7		cevlf	|- evalF
8		c2	|- 2
9	8 4	cfv	|- ( c ` 2 )
10	6 9 7	co	|- ( ( c ` 1 ) evalF ( c ` 2 ) )
11		ccofu	|- o.func
12	3	cv	|- f
13		cc0	|- 0
14	13 4	cfv	|- ( c ` 0 )
15		c1stf	|- 1stF
16	14 6 15	co	|- ( ( c ` 0 ) 1stF ( c ` 1 ) )
17	12 16 11	co	|- ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) )
18		cprf	|- pairF
19		c2ndf	|- 2ndF
20	14 6 19	co	|- ( ( c ` 0 ) 2ndF ( c ` 1 ) )
21	17 20 18	co	|- ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) )
22	10 21 11	co	|- ( ( ( c ` 1 ) evalF ( c ` 2 ) ) o.func ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) )
23	1 3 2 2 22	cmpo	|- ( c e. _V , f e. _V |-> ( ( ( c ` 1 ) evalF ( c ` 2 ) ) o.func ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) ) )
24	0 23	wceq	|- uncurryF = ( c e. _V , f e. _V |-> ( ( ( c ` 1 ) evalF ( c ` 2 ) ) o.func ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) ) )