# Metamath Proof Explorer

## Theorem cidfn

Description: The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses cidfn.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
cidfn.i
Assertion cidfn

### Proof

Step Hyp Ref Expression
1 cidfn.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 cidfn.i
3 riotaex ${⊢}\left(\iota {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)|\forall {y}\in {B}\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)\in \mathrm{V}$
4 eqid ${⊢}\left({x}\in {B}⟼\left(\iota {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)|\forall {y}\in {B}\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)=\left({x}\in {B}⟼\left(\iota {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)|\forall {y}\in {B}\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)$
5 3 4 fnmpti ${⊢}\left({x}\in {B}⟼\left(\iota {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)|\forall {y}\in {B}\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)Fn{B}$
6 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
7 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
8 id ${⊢}{C}\in \mathrm{Cat}\to {C}\in \mathrm{Cat}$
9 1 6 7 8 2 cidfval
10 9 fneq1d
11 5 10 mpbiri