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 = ( 𝑐 ∈ Cat ↦ ⟨ ( Hom_f ‘ 𝑐 ) , ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chof	⊢ Hom_F
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		chomf	⊢ Hom_f
4	1	cv	⊢ 𝑐
5	4 3	cfv	⊢ ( Hom_f ‘ 𝑐 )
6		cbs	⊢ Base
7	4 6	cfv	⊢ ( Base ‘ 𝑐 )
8		vb	⊢ 𝑏
9		vx	⊢ 𝑥
10	8	cv	⊢ 𝑏
11	10 10	cxp	⊢ ( 𝑏 × 𝑏 )
12		vy	⊢ 𝑦
13		vf	⊢ 𝑓
14		c1st	⊢ 1^st
15	12	cv	⊢ 𝑦
16	15 14	cfv	⊢ ( 1^st ‘ 𝑦 )
17		chom	⊢ Hom
18	4 17	cfv	⊢ ( Hom ‘ 𝑐 )
19	9	cv	⊢ 𝑥
20	19 14	cfv	⊢ ( 1^st ‘ 𝑥 )
21	16 20 18	co	⊢ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) )
22		vg	⊢ 𝑔
23		c2nd	⊢ 2^nd
24	19 23	cfv	⊢ ( 2^nd ‘ 𝑥 )
25	15 23	cfv	⊢ ( 2^nd ‘ 𝑦 )
26	24 25 18	co	⊢ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) )
27		vh	⊢ ℎ
28	19 18	cfv	⊢ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 )
29	22	cv	⊢ 𝑔
30		cco	⊢ comp
31	4 30	cfv	⊢ ( comp ‘ 𝑐 )
32	19 25 31	co	⊢ ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) )
33	27	cv	⊢ ℎ
34	29 33 32	co	⊢ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ )
35	16 20	cop	⊢ ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩
36	35 25 31	co	⊢ ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) )
37	13	cv	⊢ 𝑓
38	34 37 36	co	⊢ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 )
39	27 28 38	cmpt	⊢ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) )
40	13 22 21 26 39	cmpo	⊢ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) )
41	9 12 11 11 40	cmpo	⊢ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) )
42	8 7 41	csb	⊢ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) )
43	5 42	cop	⊢ ⟨ ( Hom_f ‘ 𝑐 ) , ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩
44	1 2 43	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ⟨ ( Hom_f ‘ 𝑐 ) , ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
45	0 44	wceq	⊢ Hom_F = ( 𝑐 ∈ Cat ↦ ⟨ ( Hom_f ‘ 𝑐 ) , ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )

Metamath Proof Explorer

Definition df-hof

Detailed syntax breakdown