df-evlf - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-evlf		Structured version Unicode version

Definition df-evlf 15006

Description: Define the evaluation functor, which is the extension of the evaluation map

of functors, to a functor

. (Contributed by Mario Carneiro, 11-Jan-2017.)

**Assertion**
Ref	Expression
df-evlf	eval_F Nat comp

Distinct variable group:

**Detailed syntax breakdown of Definition df-evlf**
Step	Hyp	Ref	Expression
1		cevlf 15002	. 2 eval_F
2		vc	. . 3
3		vd	. . 3
4		ccat 14585	. . 3
5		vf	. . . . 5
6		vx	. . . . 5
7	2	cv 1361	. . . . . 6
8	3	cv 1361	. . . . . 6
9		cfunc 14747	. . . . . 6
10	7, 8, 9	co 6080	. . . . 5
11		cbs 14157	. . . . . 6
12	7, 11	cfv 5406	. . . . 5
13	6	cv 1361	. . . . . 6
14	5	cv 1361	. . . . . . 7
15		c1st 6564	. . . . . . 7
16	14, 15	cfv 5406	. . . . . 6
17	13, 16	cfv 5406	. . . . 5
18	5, 6, 10, 12, 17	cmpt2 6082	. . . 4
19		vy	. . . . 5
20	10, 12	cxp 4825	. . . . 5
21		vm	. . . . . 6
22	13, 15	cfv 5406	. . . . . 6
23		vn	. . . . . . 7
24	19	cv 1361	. . . . . . . 8
25	24, 15	cfv 5406	. . . . . . 7
26		va	. . . . . . . 8
27		vg	. . . . . . . 8
28	21	cv 1361	. . . . . . . . 9
29	23	cv 1361	. . . . . . . . 9
30		cnat 14834	. . . . . . . . . 10 Nat
31	7, 8, 30	co 6080	. . . . . . . . 9 Nat
32	28, 29, 31	co 6080	. . . . . . . 8 Nat
33		c2nd 6565	. . . . . . . . . 10
34	13, 33	cfv 5406	. . . . . . . . 9
35	24, 33	cfv 5406	. . . . . . . . 9
36		chom 14232	. . . . . . . . . 10
37	7, 36	cfv 5406	. . . . . . . . 9
38	34, 35, 37	co 6080	. . . . . . . 8
39	26	cv 1361	. . . . . . . . . 10
40	35, 39	cfv 5406	. . . . . . . . 9
41	27	cv 1361	. . . . . . . . . 10
42	28, 33	cfv 5406	. . . . . . . . . . 11
43	34, 35, 42	co 6080	. . . . . . . . . 10
44	41, 43	cfv 5406	. . . . . . . . 9
45	28, 15	cfv 5406	. . . . . . . . . . . 12
46	34, 45	cfv 5406	. . . . . . . . . . 11
47	35, 45	cfv 5406	. . . . . . . . . . 11
48	46, 47	cop 3871	. . . . . . . . . 10
49	29, 15	cfv 5406	. . . . . . . . . . 11
50	35, 49	cfv 5406	. . . . . . . . . 10
51		cco 14233	. . . . . . . . . . 11 comp
52	8, 51	cfv 5406	. . . . . . . . . 10 comp
53	48, 50, 52	co 6080	. . . . . . . . 9 comp
54	40, 44, 53	co 6080	. . . . . . . 8 comp
55	26, 27, 32, 38, 54	cmpt2 6082	. . . . . . 7 Nat comp
56	23, 25, 55	csb 3276	. . . . . 6 Nat comp
57	21, 22, 56	csb 3276	. . . . 5 Nat comp
58	6, 19, 20, 20, 57	cmpt2 6082	. . . 4 Nat comp
59	18, 58	cop 3871	. . 3 Nat comp
60	2, 3, 4, 4, 59	cmpt2 6082	. 2 Nat comp
61	1, 60	wceq 1362	1 eval_F Nat comp

Colors of variables: wff setvar class

This definition is referenced by: evlfval 15010

W3C validator