Definition df-hof 17968

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 (oppCat‘𝐶) × 𝐶 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.)

Assertion

Ref	Expression
df-hof	⊢ HomF = (𝑐 ∈ Cat ↦ ⟨(Homf ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))))⟩)

Distinct variable group:   𝑏,𝑐,𝑓,𝑔,ℎ,𝑥,𝑦

Detailed syntax breakdown of Definition df-hof

Step	Hyp	Ref	Expression
1		chof 17966	. 2 class HomF
2		vc	. . 3 setvar 𝑐
3		ccat 17373	. . 3 class Cat
4	2	cv 1538	. . . . 5 class 𝑐
5		chomf 17375	. . . . 5 class Homf
6	4, 5	cfv 6433	. . . 4 class (Homf ‘𝑐)
7		vb	. . . . 5 setvar 𝑏
8		cbs 16912	. . . . . 6 class Base
9	4, 8	cfv 6433	. . . . 5 class (Base‘𝑐)
10		vx	. . . . . 6 setvar 𝑥
11		vy	. . . . . 6 setvar 𝑦
12	7	cv 1538	. . . . . . 7 class 𝑏
13	12, 12	cxp 5587	. . . . . 6 class (𝑏 × 𝑏)
14		vf	. . . . . . 7 setvar 𝑓
15		vg	. . . . . . 7 setvar 𝑔
16	11	cv 1538	. . . . . . . . 9 class 𝑦
17		c1st 7829	. . . . . . . . 9 class 1st
18	16, 17	cfv 6433	. . . . . . . 8 class (1st ‘𝑦)
19	10	cv 1538	. . . . . . . . 9 class 𝑥
20	19, 17	cfv 6433	. . . . . . . 8 class (1st ‘𝑥)
21		chom 16973	. . . . . . . . 9 class Hom
22	4, 21	cfv 6433	. . . . . . . 8 class (Hom ‘𝑐)
23	18, 20, 22	co 7275	. . . . . . 7 class ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥))
24		c2nd 7830	. . . . . . . . 9 class 2nd
25	19, 24	cfv 6433	. . . . . . . 8 class (2nd ‘𝑥)
26	16, 24	cfv 6433	. . . . . . . 8 class (2nd ‘𝑦)
27	25, 26, 22	co 7275	. . . . . . 7 class ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦))
28		vh	. . . . . . . 8 setvar ℎ
29	19, 22	cfv 6433	. . . . . . . 8 class ((Hom ‘𝑐)‘𝑥)
30	15	cv 1538	. . . . . . . . . 10 class 𝑔
31	28	cv 1538	. . . . . . . . . 10 class ℎ
32		cco 16974	. . . . . . . . . . . 12 class comp
33	4, 32	cfv 6433	. . . . . . . . . . 11 class (comp‘𝑐)
34	19, 26, 33	co 7275	. . . . . . . . . 10 class (𝑥(comp‘𝑐)(2nd ‘𝑦))
35	30, 31, 34	co 7275	. . . . . . . . 9 class (𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)
36	14	cv 1538	. . . . . . . . 9 class 𝑓
37	18, 20	cop 4567	. . . . . . . . . 10 class ⟨(1st ‘𝑦), (1st ‘𝑥)⟩
38	37, 26, 33	co 7275	. . . . . . . . 9 class (⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))
39	35, 36, 38	co 7275	. . . . . . . 8 class ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓)
40	28, 29, 39	cmpt 5157	. . . . . . 7 class (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))
41	14, 15, 23, 27, 40	cmpo 7277	. . . . . 6 class (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓)))
42	10, 11, 13, 13, 41	cmpo 7277	. . . . 5 class (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))))
43	7, 9, 42	csb 3832	. . . 4 class ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))))
44	6, 43	cop 4567	. . 3 class ⟨(Homf ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))))⟩
45	2, 3, 44	cmpt 5157	. 2 class (𝑐 ∈ Cat ↦ ⟨(Homf ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))))⟩)
46	1, 45	wceq 1539	1 wff HomF = (𝑐 ∈ Cat ↦ ⟨(Homf ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝑐)(2nd ‘𝑦))𝑓))))⟩)

This definition is referenced by:  hofval  17970