# Metamath Proof Explorer

## Theorem cidpropd

Description: Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses catpropd.1 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
catpropd.2 ${⊢}{\phi }\to {\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$
catpropd.3 ${⊢}{\phi }\to {C}\in {V}$
catpropd.4 ${⊢}{\phi }\to {D}\in {W}$
Assertion cidpropd ${⊢}{\phi }\to \mathrm{Id}\left({C}\right)=\mathrm{Id}\left({D}\right)$

### Proof

Step Hyp Ref Expression
1 catpropd.1 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
2 catpropd.2 ${⊢}{\phi }\to {\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$
3 catpropd.3 ${⊢}{\phi }\to {C}\in {V}$
4 catpropd.4 ${⊢}{\phi }\to {D}\in {W}$
5 1 homfeqbas ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{D}}$
6 5 adantr ${⊢}\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{D}}$
7 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
8 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
9 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
10 1 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
11 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to {y}\in {\mathrm{Base}}_{{C}}$
12 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
13 7 8 9 10 11 12 homfeqval ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to {y}\mathrm{Hom}\left({C}\right){x}={y}\mathrm{Hom}\left({D}\right){x}$
14 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
15 eqid ${⊢}\mathrm{comp}\left({D}\right)=\mathrm{comp}\left({D}\right)$
16 1 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
17 2 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\to {\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$
18 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
19 simp-4r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
20 simpr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\to {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)$
21 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\to {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)$
22 7 8 14 15 16 17 18 19 19 20 21 comfeqval ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\to {g}\left(⟨{y},{x}⟩\mathrm{comp}\left({C}\right){x}\right){f}={g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}$
23 22 eqeq1d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\right)\to \left({g}\left(⟨{y},{x}⟩\mathrm{comp}\left({C}\right){x}\right){f}={f}↔{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\right)$
24 13 23 raleqbidva ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to \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}↔\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\right)$
25 7 8 9 10 12 11 homfeqval ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to {x}\mathrm{Hom}\left({C}\right){y}={x}\mathrm{Hom}\left({D}\right){y}$
26 10 adantr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
27 2 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$
28 12 adantr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
29 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
30 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)$
31 simpr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)$
32 7 8 14 15 26 27 28 28 29 30 31 comfeqval ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}$
33 32 eqeq1d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to \left({f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}↔{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)$
34 25 33 raleqbidva ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to \left(\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}↔\forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)$
35 24 34 anbi12d ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to \left(\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)↔\left(\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)$
36 35 ralbidva ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\right)\to \left(\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)↔\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)$
37 36 riotabidva ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \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)=\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({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)$
38 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
39 simpr ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
40 7 8 9 38 39 39 homfeqval ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {x}\mathrm{Hom}\left({C}\right){x}={x}\mathrm{Hom}\left({D}\right){x}$
41 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{D}}$
42 41 raleqdv ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left(\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)↔\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)$
43 40 42 riotaeqbidv ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \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({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)=\left(\iota {g}\in \left({x}\mathrm{Hom}\left({D}\right){x}\right)|\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)$
44 37 43 eqtrd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \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)=\left(\iota {g}\in \left({x}\mathrm{Hom}\left({D}\right){x}\right)|\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)$
45 6 44 mpteq12dva ${⊢}\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\to \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)=\left({x}\in {\mathrm{Base}}_{{D}}⟼\left(\iota {g}\in \left({x}\mathrm{Hom}\left({D}\right){x}\right)|\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)\right)$
46 simpr ${⊢}\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\to {C}\in \mathrm{Cat}$
47 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
48 7 8 14 46 47 cidfval ${⊢}\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\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)$
49 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
50 1 2 3 4 catpropd ${⊢}{\phi }\to \left({C}\in \mathrm{Cat}↔{D}\in \mathrm{Cat}\right)$
51 50 biimpa ${⊢}\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\to {D}\in \mathrm{Cat}$
52 eqid ${⊢}\mathrm{Id}\left({D}\right)=\mathrm{Id}\left({D}\right)$
53 49 9 15 51 52 cidfval ${⊢}\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\to \mathrm{Id}\left({D}\right)=\left({x}\in {\mathrm{Base}}_{{D}}⟼\left(\iota {g}\in \left({x}\mathrm{Hom}\left({D}\right){x}\right)|\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({D}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({D}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({D}\right){y}\right){g}={f}\right)\right)\right)$
54 45 48 53 3eqtr4d ${⊢}\left({\phi }\wedge {C}\in \mathrm{Cat}\right)\to \mathrm{Id}\left({C}\right)=\mathrm{Id}\left({D}\right)$
55 simpr ${⊢}\left({\phi }\wedge ¬{C}\in \mathrm{Cat}\right)\to ¬{C}\in \mathrm{Cat}$
56 cidffn ${⊢}\mathrm{Id}Fn\mathrm{Cat}$
57 fndm ${⊢}\mathrm{Id}Fn\mathrm{Cat}\to \mathrm{dom}\mathrm{Id}=\mathrm{Cat}$
58 56 57 ax-mp ${⊢}\mathrm{dom}\mathrm{Id}=\mathrm{Cat}$
59 58 eleq2i ${⊢}{C}\in \mathrm{dom}\mathrm{Id}↔{C}\in \mathrm{Cat}$
60 55 59 sylnibr ${⊢}\left({\phi }\wedge ¬{C}\in \mathrm{Cat}\right)\to ¬{C}\in \mathrm{dom}\mathrm{Id}$
61 ndmfv ${⊢}¬{C}\in \mathrm{dom}\mathrm{Id}\to \mathrm{Id}\left({C}\right)=\varnothing$
62 60 61 syl ${⊢}\left({\phi }\wedge ¬{C}\in \mathrm{Cat}\right)\to \mathrm{Id}\left({C}\right)=\varnothing$
63 58 eleq2i ${⊢}{D}\in \mathrm{dom}\mathrm{Id}↔{D}\in \mathrm{Cat}$
64 50 63 syl6bbr ${⊢}{\phi }\to \left({C}\in \mathrm{Cat}↔{D}\in \mathrm{dom}\mathrm{Id}\right)$
65 64 notbid ${⊢}{\phi }\to \left(¬{C}\in \mathrm{Cat}↔¬{D}\in \mathrm{dom}\mathrm{Id}\right)$
66 65 biimpa ${⊢}\left({\phi }\wedge ¬{C}\in \mathrm{Cat}\right)\to ¬{D}\in \mathrm{dom}\mathrm{Id}$
67 ndmfv ${⊢}¬{D}\in \mathrm{dom}\mathrm{Id}\to \mathrm{Id}\left({D}\right)=\varnothing$
68 66 67 syl ${⊢}\left({\phi }\wedge ¬{C}\in \mathrm{Cat}\right)\to \mathrm{Id}\left({D}\right)=\varnothing$
69 62 68 eqtr4d ${⊢}\left({\phi }\wedge ¬{C}\in \mathrm{Cat}\right)\to \mathrm{Id}\left({C}\right)=\mathrm{Id}\left({D}\right)$
70 54 69 pm2.61dan ${⊢}{\phi }\to \mathrm{Id}\left({C}\right)=\mathrm{Id}\left({D}\right)$