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

Definition df-evlf 14310
 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 evalF Nat comp
Distinct variable group:   ,,,,,,,,

Detailed syntax breakdown of Definition df-evlf
StepHypRef Expression
1 cevlf 14306 . 2 evalF
2 vc . . 3
3 vd . . 3
4 ccat 13889 . . 3
5 vf . . . . 5
6 vx . . . . 5
72cv 1651 . . . . . 6
83cv 1651 . . . . . 6
9 cfunc 14051 . . . . . 6
107, 8, 9co 6081 . . . . 5
11 cbs 13469 . . . . . 6
127, 11cfv 5454 . . . . 5
136cv 1651 . . . . . 6
145cv 1651 . . . . . . 7
15 c1st 6347 . . . . . . 7
1614, 15cfv 5454 . . . . . 6
1713, 16cfv 5454 . . . . 5
185, 6, 10, 12, 17cmpt2 6083 . . . 4
19 vy . . . . 5
2010, 12cxp 4876 . . . . 5
21 vm . . . . . 6
2213, 15cfv 5454 . . . . . 6
23 vn . . . . . . 7
2419cv 1651 . . . . . . . 8
2524, 15cfv 5454 . . . . . . 7
26 va . . . . . . . 8
27 vg . . . . . . . 8
2821cv 1651 . . . . . . . . 9
2923cv 1651 . . . . . . . . 9
30 cnat 14138 . . . . . . . . . 10 Nat
317, 8, 30co 6081 . . . . . . . . 9 Nat
3228, 29, 31co 6081 . . . . . . . 8 Nat
33 c2nd 6348 . . . . . . . . . 10
3413, 33cfv 5454 . . . . . . . . 9
3524, 33cfv 5454 . . . . . . . . 9
36 chom 13540 . . . . . . . . . 10
377, 36cfv 5454 . . . . . . . . 9
3834, 35, 37co 6081 . . . . . . . 8
3926cv 1651 . . . . . . . . . 10
4035, 39cfv 5454 . . . . . . . . 9
4127cv 1651 . . . . . . . . . 10
4228, 33cfv 5454 . . . . . . . . . . 11
4334, 35, 42co 6081 . . . . . . . . . 10
4441, 43cfv 5454 . . . . . . . . 9
4528, 15cfv 5454 . . . . . . . . . . . 12
4634, 45cfv 5454 . . . . . . . . . . 11
4735, 45cfv 5454 . . . . . . . . . . 11
4846, 47cop 3817 . . . . . . . . . 10
4929, 15cfv 5454 . . . . . . . . . . 11
5035, 49cfv 5454 . . . . . . . . . 10
51 cco 13541 . . . . . . . . . . 11 comp
528, 51cfv 5454 . . . . . . . . . 10 comp
5348, 50, 52co 6081 . . . . . . . . 9 comp
5440, 44, 53co 6081 . . . . . . . 8 comp
5526, 27, 32, 38, 54cmpt2 6083 . . . . . . 7 Nat comp
5623, 25, 55csb 3251 . . . . . 6 Nat comp
5721, 22, 56csb 3251 . . . . 5 Nat comp
586, 19, 20, 20, 57cmpt2 6083 . . . 4 Nat comp
5918, 58cop 3817 . . 3 Nat comp
602, 3, 4, 4, 59cmpt2 6083 . 2 Nat comp
611, 60wceq 1652 1 evalF Nat comp
 Colors of variables: wff set class This definition is referenced by:  evlfval  14314
 Copyright terms: Public domain W3C validator