df-fuc

Description: Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in Adamek p. 87. (Contributed by Mario Carneiro, 6-Jan-2017)

		Ref	Expression
	Assertion	df-fuc	$⊢ FuncCat = (t \in Cat, u \in Cat ⟼ \{⟨{Base}_{ndx}, t Func u⟩, ⟨Hom (ndx), t Nat u⟩, ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfuc	$class FuncCat$
1		vt	$setvar t$
2		ccat	$class Cat$
3		vu	$setvar u$
4		cbs	$class Base$
5		cnx	$class ndx$
6	5 4	cfv	$class {Base}_{ndx}$
7	1	cv	$setvar t$
8		cfunc	$class Func$
9	3	cv	$setvar u$
10	7 9 8	co	$class (t Func u)$
11	6 10	cop	$class ⟨{Base}_{ndx}, t Func u⟩$
12		chom	$class Hom$
13	5 12	cfv	$class Hom (ndx)$
14		cnat	$class Nat$
15	7 9 14	co	$class (t Nat u)$
16	13 15	cop	$class ⟨Hom (ndx), t Nat u⟩$
17		cco	$class comp$
18	5 17	cfv	$class comp (ndx)$
19		vv	$setvar v$
20	10 10	cxp	$class ((t Func u) \times (t Func u))$
21		vh	$setvar h$
22		c1st	$class 1^{st}$
23	19	cv	$setvar v$
24	23 22	cfv	$class 1^{st} (v)$
25		vf	$setvar f$
26		c2nd	$class 2^{nd}$
27	23 26	cfv	$class 2^{nd} (v)$
28		vg	$setvar g$
29		vb	$setvar b$
30	28	cv	$setvar g$
31	21	cv	$setvar h$
32	30 31 15	co	$class (g (t Nat u) h)$
33		va	$setvar a$
34	25	cv	$setvar f$
35	34 30 15	co	$class (f (t Nat u) g)$
36		vx	$setvar x$
37	7 4	cfv	$class {Base}_{t}$
38	29	cv	$setvar b$
39	36	cv	$setvar x$
40	39 38	cfv	$class b (x)$
41	34 22	cfv	$class 1^{st} (f)$
42	39 41	cfv	$class 1^{st} (f) (x)$
43	30 22	cfv	$class 1^{st} (g)$
44	39 43	cfv	$class 1^{st} (g) (x)$
45	42 44	cop	$class ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩$
46	9 17	cfv	$class comp (u)$
47	31 22	cfv	$class 1^{st} (h)$
48	39 47	cfv	$class 1^{st} (h) (x)$
49	45 48 46	co	$class (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x))$
50	33	cv	$setvar a$
51	39 50	cfv	$class a (x)$
52	40 51 49	co	$class (b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))$
53	36 37 52	cmpt	$class (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))$
54	29 33 32 35 53	cmpo	$class (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x)))$
55	28 27 54	csb	$class ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x)))$
56	25 24 55	csb	$class ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x)))$
57	19 21 20 10 56	cmpo	$class (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))$
58	18 57	cop	$class ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩$
59	11 16 58	ctp	$class \{⟨{Base}_{ndx}, t Func u⟩, ⟨Hom (ndx), t Nat u⟩, ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩\}$
60	1 3 2 2 59	cmpo	$class (t \in Cat, u \in Cat ⟼ \{⟨{Base}_{ndx}, t Func u⟩, ⟨Hom (ndx), t Nat u⟩, ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩\})$
61	0 60	wceq	$wff FuncCat = (t \in Cat, u \in Cat ⟼ \{⟨{Base}_{ndx}, t Func u⟩, ⟨Hom (ndx), t Nat u⟩, ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩\})$

Metamath Proof Explorer

Definition df-fuc

Detailed syntax breakdown