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	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fuccat.r	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fuccat.s	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		fuccat.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fuccat.r	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		fuccat.s	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
5	1 2 3 4	fuccatid	⊢ ( 𝜑 → ( 𝑄 ∈ Cat ∧ ( Id ‘ 𝑄 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ 𝑓 ) ) ) ) )
6	5	simpld	⊢ ( 𝜑 → 𝑄 ∈ Cat )