Theorem idacd

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

	Ref	Expression
Hypotheses	idafval.i	|- I = ( IdA ` C )
	idafval.b	|- B = ( Base ` C )
	idafval.c	|- ( ph -> C e. Cat )
	idahom.x	|- ( ph -> X e. B )
Assertion	idacd	|- ( ph -> ( codA ` ( I ` X ) ) = X )

Proof

Step	Hyp	Ref	Expression
1		idafval.i	|- I = ( IdA ` C )
2		idafval.b	|- B = ( Base ` C )
3		idafval.c	|- ( ph -> C e. Cat )
4		idahom.x	|- ( ph -> X e. B )
5		eqid	|- ( HomA ` C ) = ( HomA ` C )
6	1 2 3 4 5	idahom	|- ( ph -> ( I ` X ) e. ( X ( HomA ` C ) X ) )
7	5	homacd	|- ( ( I ` X ) e. ( X ( HomA ` C ) X ) -> ( codA ` ( I ` X ) ) = X )
8	6 7	syl	|- ( ph -> ( codA ` ( I ` X ) ) = X )