Definition df-catc 17349

Description: Definition of the category Cat, which consists of all categories in the universe 𝑢 (i.e. "𝑢-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 "𝑢 -large categories", which can be expressed as (Cat ∖ 𝑢). (Contributed by Mario Carneiro, 3-Jan-2017.)

Assertion

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

Distinct variable group:   𝑓,𝑏,𝑔,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-catc

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

This definition is referenced by:  catcval  17350