# Metamath Proof Explorer

## Definition df-cat

Description: A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated with those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. Definition in Lang p. 53. In contrast to definition 3.1 of Adamek p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" ( ( Basec ) ), the morphisms "hom" ( ( Homc ) ) and the composition law "o" ( ( compc ) ). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in Adamek p. 21 and df-cid . (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-cat

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccat ${class}\mathrm{Cat}$
1 vc ${setvar}{c}$
2 cbs ${class}\mathrm{Base}$
3 1 cv ${setvar}{c}$
4 3 2 cfv ${class}{\mathrm{Base}}_{{c}}$
5 vb ${setvar}{b}$
6 chom ${class}\mathrm{Hom}$
7 3 6 cfv ${class}\mathrm{Hom}\left({c}\right)$
8 vh ${setvar}{h}$
9 cco ${class}\mathrm{comp}$
10 3 9 cfv ${class}\mathrm{comp}\left({c}\right)$
11 vo ${setvar}{o}$
12 vx ${setvar}{x}$
13 5 cv ${setvar}{b}$
14 vg ${setvar}{g}$
15 12 cv ${setvar}{x}$
16 8 cv ${setvar}{h}$
17 15 15 16 co ${class}\left({x}{h}{x}\right)$
18 vy ${setvar}{y}$
19 vf ${setvar}{f}$
20 18 cv ${setvar}{y}$
21 20 15 16 co ${class}\left({y}{h}{x}\right)$
22 14 cv ${setvar}{g}$
23 20 15 cop ${class}⟨{y},{x}⟩$
24 11 cv ${setvar}{o}$
25 23 15 24 co ${class}\left(⟨{y},{x}⟩{o}{x}\right)$
26 19 cv ${setvar}{f}$
27 22 26 25 co ${class}\left({g}\left(⟨{y},{x}⟩{o}{x}\right){f}\right)$
28 27 26 wceq ${wff}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}$
29 28 19 21 wral ${wff}\forall {f}\in \left({y}{h}{x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}$
30 15 20 16 co ${class}\left({x}{h}{y}\right)$
31 15 15 cop ${class}⟨{x},{x}⟩$
32 31 20 24 co ${class}\left(⟨{x},{x}⟩{o}{y}\right)$
33 26 22 32 co ${class}\left({f}\left(⟨{x},{x}⟩{o}{y}\right){g}\right)$
34 33 26 wceq ${wff}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}$
35 34 19 30 wral ${wff}\forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}$
36 29 35 wa ${wff}\left(\forall {f}\in \left({y}{h}{x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}\wedge \forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}\right)$
37 36 18 13 wral ${wff}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}{h}{x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}\wedge \forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}\right)$
38 37 14 17 wrex ${wff}\exists {g}\in \left({x}{h}{x}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}{h}{x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}\wedge \forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}\right)$
39 vz ${setvar}{z}$
40 39 cv ${setvar}{z}$
41 20 40 16 co ${class}\left({y}{h}{z}\right)$
42 15 20 cop ${class}⟨{x},{y}⟩$
43 42 40 24 co ${class}\left(⟨{x},{y}⟩{o}{z}\right)$
44 22 26 43 co ${class}\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)$
45 15 40 16 co ${class}\left({x}{h}{z}\right)$
46 44 45 wcel ${wff}{g}\left(⟨{x},{y}⟩{o}{z}\right){f}\in \left({x}{h}{z}\right)$
47 vw ${setvar}{w}$
48 vk ${setvar}{k}$
49 47 cv ${setvar}{w}$
50 40 49 16 co ${class}\left({z}{h}{w}\right)$
51 48 cv ${setvar}{k}$
52 20 40 cop ${class}⟨{y},{z}⟩$
53 52 49 24 co ${class}\left(⟨{y},{z}⟩{o}{w}\right)$
54 51 22 53 co ${class}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)$
55 42 49 24 co ${class}\left(⟨{x},{y}⟩{o}{w}\right)$
56 54 26 55 co ${class}\left(\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}\right)$
57 15 40 cop ${class}⟨{x},{z}⟩$
58 57 49 24 co ${class}\left(⟨{x},{z}⟩{o}{w}\right)$
59 51 44 58 co ${class}\left({k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)\right)$
60 56 59 wceq ${wff}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)$
61 60 48 50 wral ${wff}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)$
62 61 47 13 wral ${wff}\forall {w}\in {b}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)$
63 46 62 wa ${wff}\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\in \left({x}{h}{z}\right)\wedge \forall {w}\in {b}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)\right)$
64 63 14 41 wral ${wff}\forall {g}\in \left({y}{h}{z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\in \left({x}{h}{z}\right)\wedge \forall {w}\in {b}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)\right)$
65 64 19 30 wral ${wff}\forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{h}{z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\in \left({x}{h}{z}\right)\wedge \forall {w}\in {b}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)\right)$
66 65 39 13 wral ${wff}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{h}{z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\in \left({x}{h}{z}\right)\wedge \forall {w}\in {b}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)\right)$
67 66 18 13 wral ${wff}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{h}{z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\in \left({x}{h}{z}\right)\wedge \forall {w}\in {b}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)\right)$
68 38 67 wa ${wff}\left(\exists {g}\in \left({x}{h}{x}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}{h}{x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}\wedge \forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}\right)\wedge \forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{h}{z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\in \left({x}{h}{z}\right)\wedge \forall {w}\in {b}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)\right)\right)$
69 68 12 13 wral ${wff}\forall {x}\in {b}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \left({x}{h}{x}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}{h}{x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}\wedge \forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}\right)\wedge \forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{h}{z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\in \left({x}{h}{z}\right)\wedge \forall {w}\in {b}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}{h}{w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩{o}{w}\right){g}\right)\left(⟨{x},{y}⟩{o}{w}\right){f}={k}\left(⟨{x},{z}⟩{o}{w}\right)\left({g}\left(⟨{x},{y}⟩{o}{z}\right){f}\right)\right)\right)$
70 69 11 10 wsbc
71 70 8 7 wsbc
72 71 5 4 wsbc
73 72 1 cab
74 0 73 wceq