Theorem fucid

Description: The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucid.q	|- Q = ( C FuncCat D )
	fucid.i	|- I = ( Id ` Q )
	fucid.1	|- .1. = ( Id ` D )
	fucid.f	|- ( ph -> F e. ( C Func D ) )
Assertion	fucid	|- ( ph -> ( I ` F ) = ( .1. o. ( 1st ` F ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucid.q	|- Q = ( C FuncCat D )
2		fucid.i	|- I = ( Id ` Q )
3		fucid.1	|- .1. = ( Id ` D )
4		fucid.f	|- ( ph -> F e. ( C Func D ) )
5		funcrcl	|- ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
6	4 5	syl	|- ( ph -> ( C e. Cat /\ D e. Cat ) )
7	6	simpld	|- ( ph -> C e. Cat )
8	6	simprd	|- ( ph -> D e. Cat )
9	1 7 8 3	fuccatid	|- ( ph -> ( Q e. Cat /\ ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) ) )
10	9	simprd	|- ( ph -> ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) )
11	2 10	syl5eq	|- ( ph -> I = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) )
12		simpr	|- ( ( ph /\ f = F ) -> f = F )
13	12	fveq2d	|- ( ( ph /\ f = F ) -> ( 1st ` f ) = ( 1st ` F ) )
14	13	coeq2d	|- ( ( ph /\ f = F ) -> ( .1. o. ( 1st ` f ) ) = ( .1. o. ( 1st ` F ) ) )
15	3	fvexi	|- .1. e. _V
16		fvex	|- ( 1st ` F ) e. _V
17	15 16	coex	|- ( .1. o. ( 1st ` F ) ) e. _V
18	17	a1i	|- ( ph -> ( .1. o. ( 1st ` F ) ) e. _V )
19	11 14 4 18	fvmptd	|- ( ph -> ( I ` F ) = ( .1. o. ( 1st ` F ) ) )