# Metamath Proof Explorer

## Definition df-cid

Description: Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion df-cid

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccid ${class}\mathrm{Id}$
1 vc ${setvar}{c}$
2 ccat ${class}\mathrm{Cat}$
3 cbs ${class}\mathrm{Base}$
4 1 cv ${setvar}{c}$
5 4 3 cfv ${class}{\mathrm{Base}}_{{c}}$
6 vb ${setvar}{b}$
7 chom ${class}\mathrm{Hom}$
8 4 7 cfv ${class}\mathrm{Hom}\left({c}\right)$
9 vh ${setvar}{h}$
10 cco ${class}\mathrm{comp}$
11 4 10 cfv ${class}\mathrm{comp}\left({c}\right)$
12 vo ${setvar}{o}$
13 vx ${setvar}{x}$
14 6 cv ${setvar}{b}$
15 vg ${setvar}{g}$
16 13 cv ${setvar}{x}$
17 9 cv ${setvar}{h}$
18 16 16 17 co ${class}\left({x}{h}{x}\right)$
19 vy ${setvar}{y}$
20 vf ${setvar}{f}$
21 19 cv ${setvar}{y}$
22 21 16 17 co ${class}\left({y}{h}{x}\right)$
23 15 cv ${setvar}{g}$
24 21 16 cop ${class}⟨{y},{x}⟩$
25 12 cv ${setvar}{o}$
26 24 16 25 co ${class}\left(⟨{y},{x}⟩{o}{x}\right)$
27 20 cv ${setvar}{f}$
28 23 27 26 co ${class}\left({g}\left(⟨{y},{x}⟩{o}{x}\right){f}\right)$
29 28 27 wceq ${wff}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}$
30 29 20 22 wral ${wff}\forall {f}\in \left({y}{h}{x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩{o}{x}\right){f}={f}$
31 16 21 17 co ${class}\left({x}{h}{y}\right)$
32 16 16 cop ${class}⟨{x},{x}⟩$
33 32 21 25 co ${class}\left(⟨{x},{x}⟩{o}{y}\right)$
34 27 23 33 co ${class}\left({f}\left(⟨{x},{x}⟩{o}{y}\right){g}\right)$
35 34 27 wceq ${wff}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}$
36 35 20 31 wral ${wff}\forall {f}\in \left({x}{h}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩{o}{y}\right){g}={f}$
37 30 36 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)$
38 37 19 14 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)$
39 38 15 18 crio ${class}\left(\iota {g}\in \left({x}{h}{x}\right)|\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)\right)$
40 13 14 39 cmpt ${class}\left({x}\in {b}⟼\left(\iota {g}\in \left({x}{h}{x}\right)|\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)\right)\right)$
41 12 11 40 csb
42 9 8 41 csb
43 6 5 42 csb
44 1 2 43 cmpt
45 0 44 wceq