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	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
	diagval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diagval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	diag11.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag11.c	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	diag11.k	⊢ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 )
Assertion	diag1cl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		diagval.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
2		diagval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		diagval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		diag11.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
5		diag11.c	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
6		diag11.k	⊢ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 )
7		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
8	7	fucbas	⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
9		relfunc	⊢ Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) )
10	1 2 3 7	diagcl	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
11		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ∧ 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ) → ( 1st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2nd ‘ 𝐿 ) )
12	9 10 11	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2nd ‘ 𝐿 ) )
13	4 8 12	funcf1	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) : 𝐴 ⟶ ( 𝐷 Func 𝐶 ) )
14	13 5	ffvelrnd	⊢ ( 𝜑 → ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) )
15	6 14	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )