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	eqtrid	$$⊢\phi \to L=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$