Metamath Proof Explorer

Theorem catidcl

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catidcl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
catidcl.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
catidcl.i
catidcl.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
catidcl.x ${⊢}{\phi }\to {X}\in {B}$
Assertion catidcl

Proof

Step Hyp Ref Expression
1 catidcl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 catidcl.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 catidcl.i
4 catidcl.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
5 catidcl.x ${⊢}{\phi }\to {X}\in {B}$
6 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
7 1 2 6 4 3 5 cidval
8 1 2 6 4 5 catideu ${⊢}{\phi }\to \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}⟩\mathrm{comp}\left({C}\right){X}\right){f}={f}\wedge \forall {f}\in \left({X}{H}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{X},{X}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)$
9 riotacl ${⊢}\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}⟩\mathrm{comp}\left({C}\right){X}\right){f}={f}\wedge \forall {f}\in \left({X}{H}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{X},{X}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)\to \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}⟩\mathrm{comp}\left({C}\right){X}\right){f}={f}\wedge \forall {f}\in \left({X}{H}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{X},{X}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)\right)\in \left({X}{H}{X}\right)$
10 8 9 syl ${⊢}{\phi }\to \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}⟩\mathrm{comp}\left({C}\right){X}\right){f}={f}\wedge \forall {f}\in \left({X}{H}{y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{X},{X}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)\right)\in \left({X}{H}{X}\right)$
11 7 10 eqeltrd