# Metamath Proof Explorer

## Theorem catidd

Description: Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catidd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
catidd.h ${⊢}{\phi }\to {H}=\mathrm{Hom}\left({C}\right)$
catidd.o
catidd.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
catidd.1
catidd.2
catidd.3
Assertion catidd

### Proof

Step Hyp Ref Expression
1 catidd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
2 catidd.h ${⊢}{\phi }\to {H}=\mathrm{Hom}\left({C}\right)$
3 catidd.o
4 catidd.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
5 catidd.1
6 catidd.2
7 catidd.3
8 6 ex
9 1 eleq2d ${⊢}{\phi }\to \left({x}\in {B}↔{x}\in {\mathrm{Base}}_{{C}}\right)$
10 1 eleq2d ${⊢}{\phi }\to \left({y}\in {B}↔{y}\in {\mathrm{Base}}_{{C}}\right)$
11 2 oveqd ${⊢}{\phi }\to {y}{H}{x}={y}\mathrm{Hom}\left({C}\right){x}$
12 11 eleq2d ${⊢}{\phi }\to \left({f}\in \left({y}{H}{x}\right)↔{f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)$
13 9 10 12 3anbi123d ${⊢}{\phi }\to \left(\left({x}\in {B}\wedge {y}\in {B}\wedge {f}\in \left({y}{H}{x}\right)\right)↔\left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\right)$
14 3 oveqd
15 14 oveqd
16 15 eqeq1d
17 8 13 16 3imtr3d
18 17 3expd
19 18 imp41
20 19 ralrimiva
21 7 ex
22 2 oveqd ${⊢}{\phi }\to {x}{H}{y}={x}\mathrm{Hom}\left({C}\right){y}$
23 22 eleq2d ${⊢}{\phi }\to \left({f}\in \left({x}{H}{y}\right)↔{f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)$
24 9 10 23 3anbi123d ${⊢}{\phi }\to \left(\left({x}\in {B}\wedge {y}\in {B}\wedge {f}\in \left({x}{H}{y}\right)\right)↔\left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\right)$
25 3 oveqd
26 25 oveqd
27 26 eqeq1d
28 21 24 27 3imtr3d
29 28 3expd
30 29 imp41
31 30 ralrimiva
32 20 31 jca
33 32 ralrimiva
34 5 ex
35 2 oveqd ${⊢}{\phi }\to {x}{H}{x}={x}\mathrm{Hom}\left({C}\right){x}$
36 35 eleq2d
37 34 9 36 3imtr3d
38 37 imp
39 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
40 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
41 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
42 4 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {C}\in \mathrm{Cat}$
43 simpr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
44 39 40 41 42 43 catideu ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \exists !{g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({C}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)$
45 oveq1
46 45 eqeq1d
47 46 ralbidv
48 oveq2
49 48 eqeq1d
50 49 ralbidv
51 47 50 anbi12d
52 51 ralbidv
53 52 riota2
54 38 44 53 syl2anc
55 33 54 mpbid
56 55 mpteq2dva
57 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
58 39 40 41 4 57 cidfval ${⊢}{\phi }\to \mathrm{Id}\left({C}\right)=\left({x}\in {\mathrm{Base}}_{{C}}⟼\left(\iota {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)|\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({C}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)\right)\right)$
59 1 mpteq1d
60 56 58 59 3eqtr4d