Metamath Proof Explorer

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 Δ func D
diagval.c ⊢ φ → C ∈ Cat
diagval.d ⊢ φ → D ∈ Cat
diag11.a ⊢ A = Base C
diag11.c ⊢ φ → X ∈ A
diag11.k ⊢ K = 1 st ⁡ L ⁡ X
Assertion diag1cl ⊢ φ → K ∈ D Func C

Proof

Step Hyp Ref Expression
1 diagval.l ⊢ L = C Δ func D
2 diagval.c ⊢ φ → C ∈ Cat
3 diagval.d ⊢ φ → D ∈ Cat
4 diag11.a ⊢ A = Base C
5 diag11.c ⊢ φ → X ∈ A
6 diag11.k ⊢ K = 1 st ⁡ L ⁡ X
7 eqid ⊢ D FuncCat C = D FuncCat C
8 7 fucbas ⊢ D Func C = Base D FuncCat C
9 relfunc ⊢ Rel ⁡ C Func D FuncCat C
10 1 2 3 7 diagcl ⊢ φ → L ∈ C Func D FuncCat C
11 1st2ndbr ⊢ Rel ⁡ C Func D FuncCat C ∧ L ∈ C Func D FuncCat C → 1 st ⁡ L C Func D FuncCat C 2 nd ⁡ L
12 9 10 11 sylancr ⊢ φ → 1 st ⁡ L C Func D FuncCat C 2 nd ⁡ L
13 4 8 12 funcf1 ⊢ φ → 1 st ⁡ L : A ⟶ D Func C
14 13 5 ffvelcdmd ⊢ φ → 1 st ⁡ L ⁡ X ∈ D Func C
15 6 14 eqeltrid ⊢ φ → K ∈ D Func C