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	$⊢ {uncurry}_{F} = (c \in V, f \in V ⟼ (c (1) {eval}_{F} c (2)) \circ_{func} ((f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuncf	$class {uncurry}_{F}$
1		vc	$setvar c$
2		cvv	$class V$
3		vf	$setvar f$
4	1	cv	$setvar c$
5		c1	$class 1$
6	5 4	cfv	$class c (1)$
7		cevlf	$class {eval}_{F}$
8		c2	$class 2$
9	8 4	cfv	$class c (2)$
10	6 9 7	co	$class (c (1) {eval}_{F} c (2))$
11		ccofu	$class \circ_{func}$
12	3	cv	$setvar f$
13		cc0	$class 0$
14	13 4	cfv	$class c (0)$
15		c1stf	$class {1^{st}}_{F}$
16	14 6 15	co	$class (c (0) {1^{st}}_{F} c (1))$
17	12 16 11	co	$class (f \circ_{func} (c (0) {1^{st}}_{F} c (1)))$
18		cprf	$class {⟨,⟩}_{F}$
19		c2ndf	$class {2^{nd}}_{F}$
20	14 6 19	co	$class (c (0) {2^{nd}}_{F} c (1))$
21	17 20 18	co	$class ((f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1)))$
22	10 21 11	co	$class ((c (1) {eval}_{F} c (2)) \circ_{func} ((f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1))))$
23	1 3 2 2 22	cmpo	$class (c \in V, f \in V ⟼ (c (1) {eval}_{F} c (2)) \circ_{func} ((f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1))))$
24	0 23	wceq	$wff {uncurry}_{F} = (c \in V, f \in V ⟼ (c (1) {eval}_{F} c (2)) \circ_{func} ((f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1))))$

Metamath Proof Explorer

Definition df-uncf

Detailed syntax breakdown