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

Metamath Proof Explorer

Theorem diagcl

Description: The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor ( y e. D |-> X ) is a construction that is natural in X (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses diagval.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
diagval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
diagval.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
diagcl.q ⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
Assertion diagcl ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝑄 ) )

Proof

Step Hyp Ref Expression
1 diagval.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
2 diagval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
3 diagval.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
4 diagcl.q ⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
5 1 2 3 diagval ⊢ ( 𝜑 → 𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) )
6 eqid ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) )
7 eqid ⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
8 eqid ⊢ ( 𝐶 1stF 𝐷 ) = ( 𝐶 1stF 𝐷 )
9 7 2 3 8 1stfcl ⊢ ( 𝜑 → ( 𝐶 1stF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐶 ) )
10 6 4 2 3 9 curfcl ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) )
11 5 10 eqeltrd ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝑄 ) )