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\mathrm{FuncCat}D$$
	fuccat.r	$$⊢\phi \to C\in \mathrm{Cat}$$
	fuccat.s	$$⊢\phi \to D\in \mathrm{Cat}$$
Assertion	fuccat	$$⊢\phi \to Q\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		fuccat.q	$$⊢Q=C\mathrm{FuncCat}D$$
2		fuccat.r	$$⊢\phi \to C\in \mathrm{Cat}$$
3		fuccat.s	$$⊢\phi \to D\in \mathrm{Cat}$$
4		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
5	1 2 3 4	fuccatid	$$⊢\phi \to \left(Q\in \mathrm{Cat}\wedge \mathrm{Id}\left(Q\right)=\left(f\in \left(C\mathrm{Func}D\right)⟼\mathrm{Id}\left(D\right)\circ 1^{st}\left(f\right)\right)\right)$$
6	5	simpld	$$⊢\phi \to Q\in \mathrm{Cat}$$