Theorem idahom

Description: Domain and 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 )
	idahom.h	|- H = ( HomA ` C )
Assertion	idahom	|- ( ph -> ( I ` X ) e. ( X H 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		idahom.h	|- H = ( HomA ` C )
6		eqid	|- ( Id ` C ) = ( Id ` C )
7	1 2 3 6 4	idaval	|- ( ph -> ( I ` X ) = <. X , X , ( ( Id ` C ) ` X ) >. )
8		eqid	|- ( Hom ` C ) = ( Hom ` C )
9	2 8 6 3 4	catidcl	|- ( ph -> ( ( Id ` C ) ` X ) e. ( X ( Hom ` C ) X ) )
10	5 2 3 8 4 4 9	elhomai2	|- ( ph -> <. X , X , ( ( Id ` C ) ` X ) >. e. ( X H X ) )
11	7 10	eqeltrd	|- ( ph -> ( I ` X ) e. ( X H X ) )