Metamath Proof Explorer


Theorem diagval

Description: Define the diagonal functor, which is the functor C --> ( D Func C ) whose object part is x e. C |-> ( y e. D |-> x ) . We can define this equationally as the currying of the first projection functor, and by expressing it this way we get a quick proof of functoriality. (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses diagval.l L = C Δ func D
diagval.c φ C Cat
diagval.d φ D Cat
Assertion diagval φ L = C D curry F C 1 st F D

Proof

Step Hyp Ref Expression
1 diagval.l L = C Δ func D
2 diagval.c φ C Cat
3 diagval.d φ D Cat
4 df-diag Δ func = c Cat , d Cat c d curry F c 1 st F d
5 4 a1i φ Δ func = c Cat , d Cat c d curry F c 1 st F d
6 simprl φ c = C d = D c = C
7 simprr φ c = C d = D d = D
8 6 7 opeq12d φ c = C d = D c d = C D
9 6 7 oveq12d φ c = C d = D c 1 st F d = C 1 st F D
10 8 9 oveq12d φ c = C d = D c d curry F c 1 st F d = C D curry F C 1 st F D
11 ovexd φ C D curry F C 1 st F D V
12 5 10 2 3 11 ovmpod φ C Δ func D = C D curry F C 1 st F D
13 1 12 syl5eq φ L = C D curry F C 1 st F D