Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-evlf | Structured version Visualization version Unicode version |
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.) |
Ref | Expression |
---|---|
df-evlf | evalF Nat comp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cevlf 16849 | . 2 evalF | |
2 | vc | . . 3 | |
3 | vd | . . 3 | |
4 | ccat 16325 | . . 3 | |
5 | vf | . . . . 5 | |
6 | vx | . . . . 5 | |
7 | 2 | cv 1482 | . . . . . 6 |
8 | 3 | cv 1482 | . . . . . 6 |
9 | cfunc 16514 | . . . . . 6 | |
10 | 7, 8, 9 | co 6650 | . . . . 5 |
11 | cbs 15857 | . . . . . 6 | |
12 | 7, 11 | cfv 5888 | . . . . 5 |
13 | 6 | cv 1482 | . . . . . 6 |
14 | 5 | cv 1482 | . . . . . . 7 |
15 | c1st 7166 | . . . . . . 7 | |
16 | 14, 15 | cfv 5888 | . . . . . 6 |
17 | 13, 16 | cfv 5888 | . . . . 5 |
18 | 5, 6, 10, 12, 17 | cmpt2 6652 | . . . 4 |
19 | vy | . . . . 5 | |
20 | 10, 12 | cxp 5112 | . . . . 5 |
21 | vm | . . . . . 6 | |
22 | 13, 15 | cfv 5888 | . . . . . 6 |
23 | vn | . . . . . . 7 | |
24 | 19 | cv 1482 | . . . . . . . 8 |
25 | 24, 15 | cfv 5888 | . . . . . . 7 |
26 | va | . . . . . . . 8 | |
27 | vg | . . . . . . . 8 | |
28 | 21 | cv 1482 | . . . . . . . . 9 |
29 | 23 | cv 1482 | . . . . . . . . 9 |
30 | cnat 16601 | . . . . . . . . . 10 Nat | |
31 | 7, 8, 30 | co 6650 | . . . . . . . . 9 Nat |
32 | 28, 29, 31 | co 6650 | . . . . . . . 8 Nat |
33 | c2nd 7167 | . . . . . . . . . 10 | |
34 | 13, 33 | cfv 5888 | . . . . . . . . 9 |
35 | 24, 33 | cfv 5888 | . . . . . . . . 9 |
36 | chom 15952 | . . . . . . . . . 10 | |
37 | 7, 36 | cfv 5888 | . . . . . . . . 9 |
38 | 34, 35, 37 | co 6650 | . . . . . . . 8 |
39 | 26 | cv 1482 | . . . . . . . . . 10 |
40 | 35, 39 | cfv 5888 | . . . . . . . . 9 |
41 | 27 | cv 1482 | . . . . . . . . . 10 |
42 | 28, 33 | cfv 5888 | . . . . . . . . . . 11 |
43 | 34, 35, 42 | co 6650 | . . . . . . . . . 10 |
44 | 41, 43 | cfv 5888 | . . . . . . . . 9 |
45 | 28, 15 | cfv 5888 | . . . . . . . . . . . 12 |
46 | 34, 45 | cfv 5888 | . . . . . . . . . . 11 |
47 | 35, 45 | cfv 5888 | . . . . . . . . . . 11 |
48 | 46, 47 | cop 4183 | . . . . . . . . . 10 |
49 | 29, 15 | cfv 5888 | . . . . . . . . . . 11 |
50 | 35, 49 | cfv 5888 | . . . . . . . . . 10 |
51 | cco 15953 | . . . . . . . . . . 11 comp | |
52 | 8, 51 | cfv 5888 | . . . . . . . . . 10 comp |
53 | 48, 50, 52 | co 6650 | . . . . . . . . 9 comp |
54 | 40, 44, 53 | co 6650 | . . . . . . . 8 comp |
55 | 26, 27, 32, 38, 54 | cmpt2 6652 | . . . . . . 7 Nat comp |
56 | 23, 25, 55 | csb 3533 | . . . . . 6 Nat comp |
57 | 21, 22, 56 | csb 3533 | . . . . 5 Nat comp |
58 | 6, 19, 20, 20, 57 | cmpt2 6652 | . . . 4 Nat comp |
59 | 18, 58 | cop 4183 | . . 3 Nat comp |
60 | 2, 3, 4, 4, 59 | cmpt2 6652 | . 2 Nat comp |
61 | 1, 60 | wceq 1483 | 1 evalF Nat comp |
Colors of variables: wff setvar class |
This definition is referenced by: evlfval 16857 |
Copyright terms: Public domain | W3C validator |