Definition df-catc

Description: Definition of the category Cat, which consists of all categories in the universe u (i.e., " u -small categories", see Definition 3.44. of Adamek p. 39), with functors as the morphisms. Definition 3.47 of Adamek p. 40. We do not introduce a specific definition for " u -large categories", which can be expressed as ( Cat \ u ) . (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Assertion	df-catc	⊢ CatCat = ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Cat ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccatc	⊢ CatCat
1		vu	⊢ 𝑢
2		cvv	⊢ V
3	1	cv	⊢ 𝑢
4		ccat	⊢ Cat
5	3 4	cin	⊢ ( 𝑢 ∩ Cat )
6		vb	⊢ 𝑏
7		cbs	⊢ Base
8		cnx	⊢ ndx
9	8 7	cfv	⊢ ( Base ‘ ndx )
10	6	cv	⊢ 𝑏
11	9 10	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑏 ⟩
12		chom	⊢ Hom
13	8 12	cfv	⊢ ( Hom ‘ ndx )
14		vx	⊢ 𝑥
15		vy	⊢ 𝑦
16	14	cv	⊢ 𝑥
17		cfunc	⊢ Func
18	15	cv	⊢ 𝑦
19	16 18 17	co	⊢ ( 𝑥 Func 𝑦 )
20	14 15 10 10 19	cmpo	⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) )
21	13 20	cop	⊢ ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩
22		cco	⊢ comp
23	8 22	cfv	⊢ ( comp ‘ ndx )
24		vv	⊢ 𝑣
25	10 10	cxp	⊢ ( 𝑏 × 𝑏 )
26		vz	⊢ 𝑧
27		vg	⊢ 𝑔
28		c2nd	⊢ 2nd
29	24	cv	⊢ 𝑣
30	29 28	cfv	⊢ ( 2nd ‘ 𝑣 )
31	26	cv	⊢ 𝑧
32	30 31 17	co	⊢ ( ( 2nd ‘ 𝑣 ) Func 𝑧 )
33		vf	⊢ 𝑓
34	29 17	cfv	⊢ ( Func ‘ 𝑣 )
35	27	cv	⊢ 𝑔
36		ccofu	⊢ ∘func
37	33	cv	⊢ 𝑓
38	35 37 36	co	⊢ ( 𝑔 ∘func 𝑓 )
39	27 33 32 34 38	cmpo	⊢ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) )
40	24 26 25 10 39	cmpo	⊢ ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) )
41	23 40	cop	⊢ ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩
42	11 21 41	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ }
43	6 5 42	csb	⊢ ⦋ ( 𝑢 ∩ Cat ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ }
44	1 2 43	cmpt	⊢ ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Cat ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } )
45	0 44	wceq	⊢ CatCat = ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Cat ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } )