Theorem diag1cl

Description: The constant functor of X is a functor. (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}$$
	diag11.a	$$⊢A={\mathrm{Base}}_C$$
	diag11.c	$$⊢\phi \to X\in A$$
	diag11.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
Assertion	diag1cl	$$⊢\phi \to K\in \left(D\mathrm{Func}C\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		diag11.a	$$⊢A={\mathrm{Base}}_C$$
5		diag11.c	$$⊢\phi \to X\in A$$
6		diag11.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
7		eqid	$$⊢D\mathrm{FuncCat}C=D\mathrm{FuncCat}C$$
8	7	fucbas	$$⊢D\mathrm{Func}C={\mathrm{Base}}_{\left(D\mathrm{FuncCat}C\right)}$$
9		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)$$
10	1 2 3 7	diagcl	$$⊢\phi \to L\in \left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)$$
11		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)\wedge L\in \left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)\right)\to 1^{st}\left(L\right)\left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)2^{nd}\left(L\right)$$
12	9 10 11	sylancr	$$⊢\phi \to 1^{st}\left(L\right)\left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)2^{nd}\left(L\right)$$
13	4 8 12	funcf1	$$⊢\phi \to 1^{st}\left(L\right):A⟶D\mathrm{Func}C$$
14	13 5	ffvelcdmd	$$⊢\phi \to 1^{st}\left(L\right)\left(X\right)\in \left(D\mathrm{Func}C\right)$$
15	6 14	eqeltrid	$$⊢\phi \to K\in \left(D\mathrm{Func}C\right)$$