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 = (u \in V ⟼ ⦋ (u \cap Cat) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccatc	$class CatCat$
1		vu	$setvar u$
2		cvv	$class V$
3	1	cv	$setvar u$
4		ccat	$class Cat$
5	3 4	cin	$class (u \cap Cat)$
6		vb	$setvar b$
7		cbs	$class Base$
8		cnx	$class ndx$
9	8 7	cfv	$class {Base}_{ndx}$
10	6	cv	$setvar b$
11	9 10	cop	$class ⟨{Base}_{ndx}, b⟩$
12		chom	$class Hom$
13	8 12	cfv	$class Hom (ndx)$
14		vx	$setvar x$
15		vy	$setvar y$
16	14	cv	$setvar x$
17		cfunc	$class Func$
18	15	cv	$setvar y$
19	16 18 17	co	$class (x Func y)$
20	14 15 10 10 19	cmpo	$class (x \in b, y \in b ⟼ x Func y)$
21	13 20	cop	$class ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩$
22		cco	$class comp$
23	8 22	cfv	$class comp (ndx)$
24		vv	$setvar v$
25	10 10	cxp	$class (b \times b)$
26		vz	$setvar z$
27		vg	$setvar g$
28		c2nd	$class 2^{nd}$
29	24	cv	$setvar v$
30	29 28	cfv	$class 2^{nd} (v)$
31	26	cv	$setvar z$
32	30 31 17	co	$class (2^{nd} (v) Func z)$
33		vf	$setvar f$
34	29 17	cfv	$class Func (v)$
35	27	cv	$setvar g$
36		ccofu	$class \circ_{func}$
37	33	cv	$setvar f$
38	35 37 36	co	$class (g \circ_{func} f)$
39	27 33 32 34 38	cmpo	$class (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)$
40	24 26 25 10 39	cmpo	$class (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))$
41	23 40	cop	$class ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩$
42	11 21 41	ctp	$class \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\}$
43	6 5 42	csb	$class ⦋ (u \cap Cat) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\}$
44	1 2 43	cmpt	$class (u \in V ⟼ ⦋ (u \cap Cat) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\})$
45	0 44	wceq	$wff CatCat = (u \in V ⟼ ⦋ (u \cap Cat) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\})$

Metamath Proof Explorer

Definition df-catc

Detailed syntax breakdown