Theorem idacd

Description: Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	idafval.i	$$⊢I={Id}_a\left(C\right)$$
	idafval.b	$$⊢B={\mathrm{Base}}_C$$
	idafval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	idahom.x	$$⊢\phi \to X\in B$$
Assertion	idacd	$$⊢\phi \to {cod}_a\left(I\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		idafval.i	$$⊢I={Id}_a\left(C\right)$$
2		idafval.b	$$⊢B={\mathrm{Base}}_C$$
3		idafval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		idahom.x	$$⊢\phi \to X\in B$$
5		eqid	$$⊢{Hom}_a\left(C\right)={Hom}_a\left(C\right)$$
6	1 2 3 4 5	idahom	$$⊢\phi \to I\left(X\right)\in \left(X{Hom}_a\left(C\right)X\right)$$
7	5	homacd	$$⊢I\left(X\right)\in \left(X{Hom}_a\left(C\right)X\right)\to {cod}_a\left(I\left(X\right)\right)=X$$
8	6 7	syl	$$⊢\phi \to {cod}_a\left(I\left(X\right)\right)=X$$