df-hof

Description: Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from ( oppCatC ) X. C to SetCat , whose object part is the hom-function Hom , and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Assertion	df-hof	$⊢ {Hom}_{F} = (c \in Cat ⟼ ⟨{Hom}_{𝑓} (c), ⦋ {Base}_{c} / b ⦌ (x \in (b \times b), y \in (b \times b) ⟼ (f \in (1^{st} (y) Hom (c) 1^{st} (x)), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ (h \in Hom (c) (x) ⟼ (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f)))⟩)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chof	$class {Hom}_{F}$
1		vc	$setvar c$
2		ccat	$class Cat$
3		chomf	$class {Hom}_{𝑓}$
4	1	cv	$setvar c$
5	4 3	cfv	$class {Hom}_{𝑓} (c)$
6		cbs	$class Base$
7	4 6	cfv	$class {Base}_{c}$
8		vb	$setvar b$
9		vx	$setvar x$
10	8	cv	$setvar b$
11	10 10	cxp	$class (b \times b)$
12		vy	$setvar y$
13		vf	$setvar f$
14		c1st	$class 1^{st}$
15	12	cv	$setvar y$
16	15 14	cfv	$class 1^{st} (y)$
17		chom	$class Hom$
18	4 17	cfv	$class Hom (c)$
19	9	cv	$setvar x$
20	19 14	cfv	$class 1^{st} (x)$
21	16 20 18	co	$class (1^{st} (y) Hom (c) 1^{st} (x))$
22		vg	$setvar g$
23		c2nd	$class 2^{nd}$
24	19 23	cfv	$class 2^{nd} (x)$
25	15 23	cfv	$class 2^{nd} (y)$
26	24 25 18	co	$class (2^{nd} (x) Hom (c) 2^{nd} (y))$
27		vh	$setvar h$
28	19 18	cfv	$class Hom (c) (x)$
29	22	cv	$setvar g$
30		cco	$class comp$
31	4 30	cfv	$class comp (c)$
32	19 25 31	co	$class (x comp (c) 2^{nd} (y))$
33	27	cv	$setvar h$
34	29 33 32	co	$class (g (x comp (c) 2^{nd} (y)) h)$
35	16 20	cop	$class ⟨1^{st} (y), 1^{st} (x)⟩$
36	35 25 31	co	$class (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y))$
37	13	cv	$setvar f$
38	34 37 36	co	$class ((g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f)$
39	27 28 38	cmpt	$class (h \in Hom (c) (x) ⟼ (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f)$
40	13 22 21 26 39	cmpo	$class (f \in (1^{st} (y) Hom (c) 1^{st} (x)), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ (h \in Hom (c) (x) ⟼ (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f))$
41	9 12 11 11 40	cmpo	$class (x \in (b \times b), y \in (b \times b) ⟼ (f \in (1^{st} (y) Hom (c) 1^{st} (x)), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ (h \in Hom (c) (x) ⟼ (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f)))$
42	8 7 41	csb	$class ⦋ {Base}_{c} / b ⦌ (x \in (b \times b), y \in (b \times b) ⟼ (f \in (1^{st} (y) Hom (c) 1^{st} (x)), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ (h \in Hom (c) (x) ⟼ (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f)))$
43	5 42	cop	$class ⟨{Hom}_{𝑓} (c), ⦋ {Base}_{c} / b ⦌ (x \in (b \times b), y \in (b \times b) ⟼ (f \in (1^{st} (y) Hom (c) 1^{st} (x)), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ (h \in Hom (c) (x) ⟼ (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f)))⟩$
44	1 2 43	cmpt	$class (c \in Cat ⟼ ⟨{Hom}_{𝑓} (c), ⦋ {Base}_{c} / b ⦌ (x \in (b \times b), y \in (b \times b) ⟼ (f \in (1^{st} (y) Hom (c) 1^{st} (x)), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ (h \in Hom (c) (x) ⟼ (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f)))⟩)$
45	0 44	wceq	$wff {Hom}_{F} = (c \in Cat ⟼ ⟨{Hom}_{𝑓} (c), ⦋ {Base}_{c} / b ⦌ (x \in (b \times b), y \in (b \times b) ⟼ (f \in (1^{st} (y) Hom (c) 1^{st} (x)), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ (h \in Hom (c) (x) ⟼ (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f)))⟩)$

Metamath Proof Explorer

Definition df-hof

Detailed syntax breakdown