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

Definition df-evlf 15351
 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 15347 . 2 evalF
2 vc . . 3
3 vd . . 3
4 ccat 14933 . . 3
5 vf . . . . 5
6 vx . . . . 5
72cv 1380 . . . . . 6
83cv 1380 . . . . . 6
9 cfunc 15092 . . . . . 6
107, 8, 9co 6277 . . . . 5
11 cbs 14504 . . . . . 6
127, 11cfv 5574 . . . . 5
136cv 1380 . . . . . 6
145cv 1380 . . . . . . 7
15 c1st 6779 . . . . . . 7
1614, 15cfv 5574 . . . . . 6
1713, 16cfv 5574 . . . . 5
185, 6, 10, 12, 17cmpt2 6279 . . . 4
19 vy . . . . 5
2010, 12cxp 4983 . . . . 5
21 vm . . . . . 6
2213, 15cfv 5574 . . . . . 6
23 vn . . . . . . 7
2419cv 1380 . . . . . . . 8
2524, 15cfv 5574 . . . . . . 7
26 va . . . . . . . 8
27 vg . . . . . . . 8
2821cv 1380 . . . . . . . . 9
2923cv 1380 . . . . . . . . 9
30 cnat 15179 . . . . . . . . . 10 Nat
317, 8, 30co 6277 . . . . . . . . 9 Nat
3228, 29, 31co 6277 . . . . . . . 8 Nat
33 c2nd 6780 . . . . . . . . . 10
3413, 33cfv 5574 . . . . . . . . 9
3524, 33cfv 5574 . . . . . . . . 9
36 chom 14580 . . . . . . . . . 10
377, 36cfv 5574 . . . . . . . . 9
3834, 35, 37co 6277 . . . . . . . 8
3926cv 1380 . . . . . . . . . 10
4035, 39cfv 5574 . . . . . . . . 9
4127cv 1380 . . . . . . . . . 10
4228, 33cfv 5574 . . . . . . . . . . 11
4334, 35, 42co 6277 . . . . . . . . . 10
4441, 43cfv 5574 . . . . . . . . 9
4528, 15cfv 5574 . . . . . . . . . . . 12
4634, 45cfv 5574 . . . . . . . . . . 11
4735, 45cfv 5574 . . . . . . . . . . 11
4846, 47cop 4016 . . . . . . . . . 10
4929, 15cfv 5574 . . . . . . . . . . 11
5035, 49cfv 5574 . . . . . . . . . 10
51 cco 14581 . . . . . . . . . . 11 comp
528, 51cfv 5574 . . . . . . . . . 10 comp
5348, 50, 52co 6277 . . . . . . . . 9 comp
5440, 44, 53co 6277 . . . . . . . 8 comp
5526, 27, 32, 38, 54cmpt2 6279 . . . . . . 7 Nat comp
5623, 25, 55csb 3417 . . . . . 6 Nat comp
5721, 22, 56csb 3417 . . . . 5 Nat comp
586, 19, 20, 20, 57cmpt2 6279 . . . 4 Nat comp
5918, 58cop 4016 . . 3 Nat comp
602, 3, 4, 4, 59cmpt2 6279 . 2 Nat comp
611, 60wceq 1381 1 evalF Nat comp
 Colors of variables: wff setvar class This definition is referenced by:  evlfval  15355
 Copyright terms: Public domain W3C validator