Theorem diag2cl

Description: The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017)

	Ref	Expression
Hypotheses	diag2.l	|- L = ( C DiagFunc D )
	diag2.a	|- A = ( Base ` C )
	diag2.b	|- B = ( Base ` D )
	diag2.h	|- H = ( Hom ` C )
	diag2.c	|- ( ph -> C e. Cat )
	diag2.d	|- ( ph -> D e. Cat )
	diag2.x	|- ( ph -> X e. A )
	diag2.y	|- ( ph -> Y e. A )
	diag2.f	|- ( ph -> F e. ( X H Y ) )
	diag2cl.h	|- N = ( D Nat C )
Assertion	diag2cl	|- ( ph -> ( B X. { F } ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		diag2.l	|- L = ( C DiagFunc D )
2		diag2.a	|- A = ( Base ` C )
3		diag2.b	|- B = ( Base ` D )
4		diag2.h	|- H = ( Hom ` C )
5		diag2.c	|- ( ph -> C e. Cat )
6		diag2.d	|- ( ph -> D e. Cat )
7		diag2.x	|- ( ph -> X e. A )
8		diag2.y	|- ( ph -> Y e. A )
9		diag2.f	|- ( ph -> F e. ( X H Y ) )
10		diag2cl.h	|- N = ( D Nat C )
11	1 2 3 4 5 6 7 8 9	diag2	|- ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( B X. { F } ) )
12		eqid	|- ( D FuncCat C ) = ( D FuncCat C )
13	12 10	fuchom	|- N = ( Hom ` ( D FuncCat C ) )
14		relfunc	|- Rel ( C Func ( D FuncCat C ) )
15	1 5 6 12	diagcl	|- ( ph -> L e. ( C Func ( D FuncCat C ) ) )
16		1st2ndbr	|- ( ( Rel ( C Func ( D FuncCat C ) ) /\ L e. ( C Func ( D FuncCat C ) ) ) -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
17	14 15 16	sylancr	|- ( ph -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
18	2 4 13 17 7 8	funcf2	|- ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) --> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
19	18 9	ffvelrnd	|- ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
20	11 19	eqeltrrd	|- ( ph -> ( B X. { F } ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )