Theorem fuccat

Description: The functor category is a category. Remark 6.16 in Adamek p. 88. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fuccat.q	|- Q = ( C FuncCat D )
	fuccat.r	|- ( ph -> C e. Cat )
	fuccat.s	|- ( ph -> D e. Cat )
Assertion	fuccat	|- ( ph -> Q e. Cat )

Proof

Step	Hyp	Ref	Expression
1		fuccat.q	|- Q = ( C FuncCat D )
2		fuccat.r	|- ( ph -> C e. Cat )
3		fuccat.s	|- ( ph -> D e. Cat )
4		eqid	|- ( Id ` D ) = ( Id ` D )
5	1 2 3 4	fuccatid	|- ( ph -> ( Q e. Cat /\ ( Id ` Q ) = ( f e. ( C Func D ) |-> ( ( Id ` D ) o. ( 1st ` f ) ) ) ) )
6	5	simpld	|- ( ph -> Q e. Cat )