This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐿 = ( 𝐶 Δ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 ffvelcdmd ⊢ ( 𝜑 → ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) )
15 6 14 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )