This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )