Theorem catidcl

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	catidcl.b	|- B = ( Base ` C )
	catidcl.h	|- H = ( Hom ` C )
	catidcl.i	|- .1. = ( Id ` C )
	catidcl.c	|- ( ph -> C e. Cat )
	catidcl.x	|- ( ph -> X e. B )
Assertion	catidcl	|- ( ph -> ( .1. ` X ) e. ( X H X ) )

Proof

Step	Hyp	Ref	Expression
1		catidcl.b	|- B = ( Base ` C )
2		catidcl.h	|- H = ( Hom ` C )
3		catidcl.i	|- .1. = ( Id ` C )
4		catidcl.c	|- ( ph -> C e. Cat )
5		catidcl.x	|- ( ph -> X e. B )
6		eqid	|- ( comp ` C ) = ( comp ` C )
7	1 2 6 4 3 5	cidval	|- ( ph -> ( .1. ` X ) = ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. ( comp ` C ) X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. ( comp ` C ) y ) g ) = f ) ) )
8	1 2 6 4 5	catideu	|- ( ph -> E! g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. ( comp ` C ) X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. ( comp ` C ) y ) g ) = f ) )
9		riotacl	|- ( E! g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. ( comp ` C ) X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. ( comp ` C ) y ) g ) = f ) -> ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. ( comp ` C ) X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. ( comp ` C ) y ) g ) = f ) ) e. ( X H X ) )
10	8 9	syl	|- ( ph -> ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. ( comp ` C ) X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. ( comp ` C ) y ) g ) = f ) ) e. ( X H X ) )
11	7 10	eqeltrd	|- ( ph -> ( .1. ` X ) e. ( X H X ) )