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}{\Delta }_{\mathrm{func}}{D}$
diagval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
diagval.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
Assertion diagval ${⊢}{\phi }\to {L}=⟨{C},{D}⟩{curry}_{F}\left({C}{{1}^{st}}_{F}{D}\right)$

Proof

Step Hyp Ref Expression
1 diagval.l ${⊢}{L}={C}{\Delta }_{\mathrm{func}}{D}$
2 diagval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
3 diagval.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
4 df-diag ${⊢}{\Delta }_{\mathrm{func}}=\left({c}\in \mathrm{Cat},{d}\in \mathrm{Cat}⟼⟨{c},{d}⟩{curry}_{F}\left({c}{{1}^{st}}_{F}{d}\right)\right)$
5 4 a1i ${⊢}{\phi }\to {\Delta }_{\mathrm{func}}=\left({c}\in \mathrm{Cat},{d}\in \mathrm{Cat}⟼⟨{c},{d}⟩{curry}_{F}\left({c}{{1}^{st}}_{F}{d}\right)\right)$
6 simprl ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {d}={D}\right)\right)\to {c}={C}$
7 simprr ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {d}={D}\right)\right)\to {d}={D}$
8 6 7 opeq12d ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {d}={D}\right)\right)\to ⟨{c},{d}⟩=⟨{C},{D}⟩$
9 6 7 oveq12d ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {d}={D}\right)\right)\to {c}{{1}^{st}}_{F}{d}={C}{{1}^{st}}_{F}{D}$
10 8 9 oveq12d ${⊢}\left({\phi }\wedge \left({c}={C}\wedge {d}={D}\right)\right)\to ⟨{c},{d}⟩{curry}_{F}\left({c}{{1}^{st}}_{F}{d}\right)=⟨{C},{D}⟩{curry}_{F}\left({C}{{1}^{st}}_{F}{D}\right)$
11 ovexd ${⊢}{\phi }\to ⟨{C},{D}⟩{curry}_{F}\left({C}{{1}^{st}}_{F}{D}\right)\in \mathrm{V}$
12 5 10 2 3 11 ovmpod ${⊢}{\phi }\to {C}{\Delta }_{\mathrm{func}}{D}=⟨{C},{D}⟩{curry}_{F}\left({C}{{1}^{st}}_{F}{D}\right)$
13 1 12 syl5eq ${⊢}{\phi }\to {L}=⟨{C},{D}⟩{curry}_{F}\left({C}{{1}^{st}}_{F}{D}\right)$