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 DiagFunc D )
diagval.c 
|- ( ph -> C e. Cat )
diagval.d 
|- ( ph -> D e. Cat )
diag11.a 
|- A = ( Base ` C )
diag11.c 
|- ( ph -> X e. A )
diag11.k 
|- K = ( ( 1st ` L ) ` X )
Assertion diag1cl 
|- ( ph -> K e. ( D Func C ) )

Proof

Step Hyp Ref Expression
1 diagval.l 
 |-  L = ( C DiagFunc D )
2 diagval.c 
 |-  ( ph -> C e. Cat )
3 diagval.d 
 |-  ( ph -> D e. Cat )
4 diag11.a 
 |-  A = ( Base ` C )
5 diag11.c 
 |-  ( ph -> X e. A )
6 diag11.k 
 |-  K = ( ( 1st ` 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 
 |-  ( ph -> L e. ( C Func ( D FuncCat C ) ) )
11 1st2ndbr 
 |-  ( ( Rel ( C Func ( D FuncCat C ) ) /\ L e. ( C Func ( D FuncCat C ) ) ) -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
12 9 10 11 sylancr 
 |-  ( ph -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
13 4 8 12 funcf1 
 |-  ( ph -> ( 1st ` L ) : A --> ( D Func C ) )
14 13 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` L ) ` X ) e. ( D Func C ) )
15 6 14 eqeltrid 
 |-  ( ph -> K e. ( D Func C ) )