Theorem idahom

Description: Domain and 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$$
	idahom.h	$$⊢H={Hom}_a\left(C\right)$$
Assertion	idahom	$$⊢\phi \to I\left(X\right)\in \left(XHX\right)$$

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		idahom.h	$$⊢H={Hom}_a\left(C\right)$$
6		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
7	1 2 3 6 4	idaval	$$⊢\phi \to I\left(X\right)=⟨X,X,\mathrm{Id}\left(C\right)\left(X\right)⟩$$
8		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
9	2 8 6 3 4	catidcl	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)$$
10	5 2 3 8 4 4 9	elhomai2	$$⊢\phi \to ⟨X,X,\mathrm{Id}\left(C\right)\left(X\right)⟩\in \left(XHX\right)$$
11	7 10	eqeltrd	$$⊢\phi \to I\left(X\right)\in \left(XHX\right)$$