Metamath Proof Explorer

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 ( catchom , elcatchom ). 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 ∈ V ⟼ ⦋ u ∩ Cat / b⦌ Base ndx b Hom ⁡ ndx x ∈ b , y ∈ b ⟼ x Func y comp ⁡ ndx v ∈ b × b , z ∈ b ⟼ g ∈ 2 nd ⁡ v Func z , f ∈ Func ⁡ v ⟼ g ∘ 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 ∩ 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 ∈ b , y ∈ b ⟼ x Func y
21 13 20 cop class Hom ⁡ ndx x ∈ b , y ∈ 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 × 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 ∘ func
37 33 cv setvar f
38 35 37 36 co class g ∘ func f
39 27 33 32 34 38 cmpo class g ∈ 2 nd ⁡ v Func z , f ∈ Func ⁡ v ⟼ g ∘ func f
40 24 26 25 10 39 cmpo class v ∈ b × b , z ∈ b ⟼ g ∈ 2 nd ⁡ v Func z , f ∈ Func ⁡ v ⟼ g ∘ func f
41 23 40 cop class comp ⁡ ndx v ∈ b × b , z ∈ b ⟼ g ∈ 2 nd ⁡ v Func z , f ∈ Func ⁡ v ⟼ g ∘ func f
42 11 21 41 ctp class Base ndx b Hom ⁡ ndx x ∈ b , y ∈ b ⟼ x Func y comp ⁡ ndx v ∈ b × b , z ∈ b ⟼ g ∈ 2 nd ⁡ v Func z , f ∈ Func ⁡ v ⟼ g ∘ func f
43 6 5 42 csb class ⦋ u ∩ Cat / b⦌ Base ndx b Hom ⁡ ndx x ∈ b , y ∈ b ⟼ x Func y comp ⁡ ndx v ∈ b × b , z ∈ b ⟼ g ∈ 2 nd ⁡ v Func z , f ∈ Func ⁡ v ⟼ g ∘ func f
44 1 2 43 cmpt class u ∈ V ⟼ ⦋ u ∩ Cat / b⦌ Base ndx b Hom ⁡ ndx x ∈ b , y ∈ b ⟼ x Func y comp ⁡ ndx v ∈ b × b , z ∈ b ⟼ g ∈ 2 nd ⁡ v Func z , f ∈ Func ⁡ v ⟼ g ∘ func f
45 0 44 wceq wff CatCat = u ∈ V ⟼ ⦋ u ∩ Cat / b⦌ Base ndx b Hom ⁡ ndx x ∈ b , y ∈ b ⟼ x Func y comp ⁡ ndx v ∈ b × b , z ∈ b ⟼ g ∈ 2 nd ⁡ v Func z , f ∈ Func ⁡ v ⟼ g ∘ func f