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

Definition df-catc 14250
 Description: Definition of the category Cat, which consists of all categories in the universe , with functors as the morphisms. (Contributed by Mario Carneiro, 3-Jan-2017.)
Assertion
Ref Expression
df-catc CatCat comp func
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-catc
StepHypRef Expression
1 ccatc 14249 . 2 CatCat
2 vu . . 3
3 cvv 2956 . . 3
4 vb . . . 4
52cv 1651 . . . . 5
6 ccat 13889 . . . . 5
75, 6cin 3319 . . . 4
8 cnx 13466 . . . . . . 7
9 cbs 13469 . . . . . . 7
108, 9cfv 5454 . . . . . 6
114cv 1651 . . . . . 6
1210, 11cop 3817 . . . . 5
13 chom 13540 . . . . . . 7
148, 13cfv 5454 . . . . . 6
15 vx . . . . . . 7
16 vy . . . . . . 7
1715cv 1651 . . . . . . . 8
1816cv 1651 . . . . . . . 8
19 cfunc 14051 . . . . . . . 8
2017, 18, 19co 6081 . . . . . . 7
2115, 16, 11, 11, 20cmpt2 6083 . . . . . 6
2214, 21cop 3817 . . . . 5
23 cco 13541 . . . . . . 7 comp
248, 23cfv 5454 . . . . . 6 comp
25 vv . . . . . . 7
26 vz . . . . . . 7
2711, 11cxp 4876 . . . . . . 7
28 vg . . . . . . . 8
29 vf . . . . . . . 8
3025cv 1651 . . . . . . . . . 10
31 c2nd 6348 . . . . . . . . . 10
3230, 31cfv 5454 . . . . . . . . 9
3326cv 1651 . . . . . . . . 9
3432, 33, 19co 6081 . . . . . . . 8
3530, 19cfv 5454 . . . . . . . 8
3628cv 1651 . . . . . . . . 9
3729cv 1651 . . . . . . . . 9
38 ccofu 14053 . . . . . . . . 9 func
3936, 37, 38co 6081 . . . . . . . 8 func
4028, 29, 34, 35, 39cmpt2 6083 . . . . . . 7 func
4125, 26, 27, 11, 40cmpt2 6083 . . . . . 6 func
4224, 41cop 3817 . . . . 5 comp func
4312, 22, 42ctp 3816 . . . 4 comp func
444, 7, 43csb 3251 . . 3 comp func
452, 3, 44cmpt 4266 . 2 comp func
461, 45wceq 1652 1 CatCat comp func
 Colors of variables: wff set class This definition is referenced by:  catcval  14251
 Copyright terms: Public domain W3C validator