This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑢 ∈ 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 𝑓 ) ) ) ⟩ } )