df-evlf

Description: Define the evaluation functor, which is the extension of the evaluation map f , x |-> ( fx ) of functors, to a functor ( C --> D ) X. C --> D . (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Assertion	df-evlf	$⊢ {eval}_{F} = (c \in Cat, d \in Cat ⟼ ⟨(f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x)), (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cevlf	$class {eval}_{F}$
1		vc	$setvar c$
2		ccat	$class Cat$
3		vd	$setvar d$
4		vf	$setvar f$
5	1	cv	$setvar c$
6		cfunc	$class Func$
7	3	cv	$setvar d$
8	5 7 6	co	$class (c Func d)$
9		vx	$setvar x$
10		cbs	$class Base$
11	5 10	cfv	$class {Base}_{c}$
12		c1st	$class 1^{st}$
13	4	cv	$setvar f$
14	13 12	cfv	$class 1^{st} (f)$
15	9	cv	$setvar x$
16	15 14	cfv	$class 1^{st} (f) (x)$
17	4 9 8 11 16	cmpo	$class (f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x))$
18	8 11	cxp	$class ((c Func d) \times {Base}_{c})$
19		vy	$setvar y$
20	15 12	cfv	$class 1^{st} (x)$
21		vm	$setvar m$
22	19	cv	$setvar y$
23	22 12	cfv	$class 1^{st} (y)$
24		vn	$setvar n$
25		va	$setvar a$
26	21	cv	$setvar m$
27		cnat	$class Nat$
28	5 7 27	co	$class (c Nat d)$
29	24	cv	$setvar n$
30	26 29 28	co	$class (m (c Nat d) n)$
31		vg	$setvar g$
32		c2nd	$class 2^{nd}$
33	15 32	cfv	$class 2^{nd} (x)$
34		chom	$class Hom$
35	5 34	cfv	$class Hom (c)$
36	22 32	cfv	$class 2^{nd} (y)$
37	33 36 35	co	$class (2^{nd} (x) Hom (c) 2^{nd} (y))$
38	25	cv	$setvar a$
39	36 38	cfv	$class a (2^{nd} (y))$
40	26 12	cfv	$class 1^{st} (m)$
41	33 40	cfv	$class 1^{st} (m) (2^{nd} (x))$
42	36 40	cfv	$class 1^{st} (m) (2^{nd} (y))$
43	41 42	cop	$class ⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩$
44		cco	$class comp$
45	7 44	cfv	$class comp (d)$
46	29 12	cfv	$class 1^{st} (n)$
47	36 46	cfv	$class 1^{st} (n) (2^{nd} (y))$
48	43 47 45	co	$class (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y)))$
49	26 32	cfv	$class 2^{nd} (m)$
50	33 36 49	co	$class (2^{nd} (x) 2^{nd} (m) 2^{nd} (y))$
51	31	cv	$setvar g$
52	51 50	cfv	$class (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)$
53	39 52 48	co	$class (a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))$
54	25 31 30 37 53	cmpo	$class (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))$
55	24 23 54	csb	$class ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))$
56	21 20 55	csb	$class ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))$
57	9 19 18 18 56	cmpo	$class (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))$
58	17 57	cop	$class ⟨(f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x)), (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩$
59	1 3 2 2 58	cmpo	$class (c \in Cat, d \in Cat ⟼ ⟨(f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x)), (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩)$
60	0 59	wceq	$wff {eval}_{F} = (c \in Cat, d \in Cat ⟼ ⟨(f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x)), (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩)$

Metamath Proof Explorer

Definition df-evlf

Detailed syntax breakdown