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 = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfuc	⊢ FuncCat
1		vt	⊢ 𝑡
2		ccat	⊢ Cat
3		vu	⊢ 𝑢
4		cbs	⊢ Base
5		cnx	⊢ ndx
6	5 4	cfv	⊢ ( Base ‘ ndx )
7	1	cv	⊢ 𝑡
8		cfunc	⊢ Func
9	3	cv	⊢ 𝑢
10	7 9 8	co	⊢ ( 𝑡 Func 𝑢 )
11	6 10	cop	⊢ ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩
12		chom	⊢ Hom
13	5 12	cfv	⊢ ( Hom ‘ ndx )
14		cnat	⊢ Nat
15	7 9 14	co	⊢ ( 𝑡 Nat 𝑢 )
16	13 15	cop	⊢ ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩
17		cco	⊢ comp
18	5 17	cfv	⊢ ( comp ‘ ndx )
19		vv	⊢ 𝑣
20	10 10	cxp	⊢ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) )
21		vh	⊢ ℎ
22		c1st	⊢ 1^st
23	19	cv	⊢ 𝑣
24	23 22	cfv	⊢ ( 1^st ‘ 𝑣 )
25		vf	⊢ 𝑓
26		c2nd	⊢ 2^nd
27	23 26	cfv	⊢ ( 2^nd ‘ 𝑣 )
28		vg	⊢ 𝑔
29		vb	⊢ 𝑏
30	28	cv	⊢ 𝑔
31	21	cv	⊢ ℎ
32	30 31 15	co	⊢ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ )
33		va	⊢ 𝑎
34	25	cv	⊢ 𝑓
35	34 30 15	co	⊢ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 )
36		vx	⊢ 𝑥
37	7 4	cfv	⊢ ( Base ‘ 𝑡 )
38	29	cv	⊢ 𝑏
39	36	cv	⊢ 𝑥
40	39 38	cfv	⊢ ( 𝑏 ‘ 𝑥 )
41	34 22	cfv	⊢ ( 1^st ‘ 𝑓 )
42	39 41	cfv	⊢ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 )
43	30 22	cfv	⊢ ( 1^st ‘ 𝑔 )
44	39 43	cfv	⊢ ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 )
45	42 44	cop	⊢ ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩
46	9 17	cfv	⊢ ( comp ‘ 𝑢 )
47	31 22	cfv	⊢ ( 1^st ‘ ℎ )
48	39 47	cfv	⊢ ( ( 1^st ‘ ℎ ) ‘ 𝑥 )
49	45 48 46	co	⊢ ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) )
50	33	cv	⊢ 𝑎
51	39 50	cfv	⊢ ( 𝑎 ‘ 𝑥 )
52	40 51 49	co	⊢ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) )
53	36 37 52	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) )
54	29 33 32 35 53	cmpo	⊢ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
55	28 27 54	csb	⊢ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
56	25 24 55	csb	⊢ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
57	19 21 20 10 56	cmpo	⊢ ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
58	18 57	cop	⊢ ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩
59	11 16 58	ctp	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ }
60	1 3 2 2 59	cmpo	⊢ ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
61	0 60	wceq	⊢ FuncCat = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )

Metamath Proof Explorer

Definition df-fuc

Detailed syntax breakdown