Theorem catcid

Description: The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	catccatid.c	|- C = ( CatCat ` U )
	catccatid.b	|- B = ( Base ` C )
	catcid.o	|- .1. = ( Id ` C )
	catcid.i	|- I = ( idFunc ` X )
	catcid.u	|- ( ph -> U e. V )
	catcid.x	|- ( ph -> X e. B )
Assertion	catcid	|- ( ph -> ( .1. ` X ) = I )

Proof

Step	Hyp	Ref	Expression
1		catccatid.c	|- C = ( CatCat ` U )
2		catccatid.b	|- B = ( Base ` C )
3		catcid.o	|- .1. = ( Id ` C )
4		catcid.i	|- I = ( idFunc ` X )
5		catcid.u	|- ( ph -> U e. V )
6		catcid.x	|- ( ph -> X e. B )
7	1 2	catccatid	|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( idFunc ` x ) ) ) )
8	5 7	syl	|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( idFunc ` x ) ) ) )
9	8	simprd	|- ( ph -> ( Id ` C ) = ( x e. B |-> ( idFunc ` x ) ) )
10	3 9	syl5eq	|- ( ph -> .1. = ( x e. B |-> ( idFunc ` x ) ) )
11		simpr	|- ( ( ph /\ x = X ) -> x = X )
12	11	fveq2d	|- ( ( ph /\ x = X ) -> ( idFunc ` x ) = ( idFunc ` X ) )
13		fvexd	|- ( ph -> ( idFunc ` X ) e. _V )
14	10 12 6 13	fvmptd	|- ( ph -> ( .1. ` X ) = ( idFunc ` X ) )
15	14 4	eqtr4di	|- ( ph -> ( .1. ` X ) = I )