MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-catc Structured version   Visualization version   GIF version

Definition df-catc 17990
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
StepHypRef Expression
1 ccatc 17989 . 2 class CatCat
2 vu . . 3 setvar 𝑒
3 cvv 3444 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1541 . . . . 5 class 𝑒
6 ccat 17549 . . . . 5 class Cat
75, 6cin 3910 . . . 4 class (𝑒 ∩ Cat)
8 cnx 17070 . . . . . . 7 class ndx
9 cbs 17088 . . . . . . 7 class Base
108, 9cfv 6497 . . . . . 6 class (Baseβ€˜ndx)
114cv 1541 . . . . . 6 class 𝑏
1210, 11cop 4593 . . . . 5 class ⟨(Baseβ€˜ndx), π‘βŸ©
13 chom 17149 . . . . . . 7 class Hom
148, 13cfv 6497 . . . . . 6 class (Hom β€˜ndx)
15 vx . . . . . . 7 setvar π‘₯
16 vy . . . . . . 7 setvar 𝑦
1715cv 1541 . . . . . . . 8 class π‘₯
1816cv 1541 . . . . . . . 8 class 𝑦
19 cfunc 17745 . . . . . . . 8 class Func
2017, 18, 19co 7358 . . . . . . 7 class (π‘₯ Func 𝑦)
2115, 16, 11, 11, 20cmpo 7360 . . . . . 6 class (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ Func 𝑦))
2214, 21cop 4593 . . . . 5 class ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ Func 𝑦))⟩
23 cco 17150 . . . . . . 7 class comp
248, 23cfv 6497 . . . . . 6 class (compβ€˜ndx)
25 vv . . . . . . 7 setvar 𝑣
26 vz . . . . . . 7 setvar 𝑧
2711, 11cxp 5632 . . . . . . 7 class (𝑏 Γ— 𝑏)
28 vg . . . . . . . 8 setvar 𝑔
29 vf . . . . . . . 8 setvar 𝑓
3025cv 1541 . . . . . . . . . 10 class 𝑣
31 c2nd 7921 . . . . . . . . . 10 class 2nd
3230, 31cfv 6497 . . . . . . . . 9 class (2nd β€˜π‘£)
3326cv 1541 . . . . . . . . 9 class 𝑧
3432, 33, 19co 7358 . . . . . . . 8 class ((2nd β€˜π‘£) Func 𝑧)
3530, 19cfv 6497 . . . . . . . 8 class ( Func β€˜π‘£)
3628cv 1541 . . . . . . . . 9 class 𝑔
3729cv 1541 . . . . . . . . 9 class 𝑓
38 ccofu 17747 . . . . . . . . 9 class ∘func
3936, 37, 38co 7358 . . . . . . . 8 class (𝑔 ∘func 𝑓)
4028, 29, 34, 35, 39cmpo 7360 . . . . . . 7 class (𝑔 ∈ ((2nd β€˜π‘£) Func 𝑧), 𝑓 ∈ ( Func β€˜π‘£) ↦ (𝑔 ∘func 𝑓))
4125, 26, 27, 11, 40cmpo 7360 . . . . . 6 class (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) Func 𝑧), 𝑓 ∈ ( Func β€˜π‘£) ↦ (𝑔 ∘func 𝑓)))
4224, 41cop 4593 . . . . 5 class ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) Func 𝑧), 𝑓 ∈ ( Func β€˜π‘£) ↦ (𝑔 ∘func 𝑓)))⟩
4312, 22, 42ctp 4591 . . . 4 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ Func 𝑦))⟩, ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) Func 𝑧), 𝑓 ∈ ( Func β€˜π‘£) ↦ (𝑔 ∘func 𝑓)))⟩}
444, 7, 43csb 3856 . . 3 class ⦋(𝑒 ∩ Cat) / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ Func 𝑦))⟩, ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) Func 𝑧), 𝑓 ∈ ( Func β€˜π‘£) ↦ (𝑔 ∘func 𝑓)))⟩}
452, 3, 44cmpt 5189 . 2 class (𝑒 ∈ V ↦ ⦋(𝑒 ∩ Cat) / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ Func 𝑦))⟩, ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) Func 𝑧), 𝑓 ∈ ( Func β€˜π‘£) ↦ (𝑔 ∘func 𝑓)))⟩})
461, 45wceq 1542 1 wff CatCat = (𝑒 ∈ V ↦ ⦋(𝑒 ∩ Cat) / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ Func 𝑦))⟩, ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) Func 𝑧), 𝑓 ∈ ( Func β€˜π‘£) ↦ (𝑔 ∘func 𝑓)))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  catcval  17991
  Copyright terms: Public domain W3C validator