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	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
	diag2.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	diag2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	diag2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diag2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	diag2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	diag2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	diag2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	diag2cl.h	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
Assertion	diag2cl	⊢ ( 𝜑 → ( 𝐵 × { 𝐹 } ) ∈ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1st ‘ 𝐿 ) ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		diag2.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
2		diag2.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		diag2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
4		diag2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		diag2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6		diag2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
7		diag2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		diag2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
9		diag2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
10		diag2cl.h	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
11	1 2 3 4 5 6 7 8 9	diag2	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) = ( 𝐵 × { 𝐹 } ) )
12		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
13	12 10	fuchom	⊢ 𝑁 = ( Hom ‘ ( 𝐷 FuncCat 𝐶 ) )
14		relfunc	⊢ Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) )
15	1 5 6 12	diagcl	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
16		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ∧ 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ) → ( 1st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2nd ‘ 𝐿 ) )
17	14 15 16	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2nd ‘ 𝐿 ) )
18	2 4 13 17 7 8	funcf2	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1st ‘ 𝐿 ) ‘ 𝑌 ) ) )
19	18 9	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) ∈ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1st ‘ 𝐿 ) ‘ 𝑌 ) ) )
20	11 19	eqeltrrd	⊢ ( 𝜑 → ( 𝐵 × { 𝐹 } ) ∈ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1st ‘ 𝐿 ) ‘ 𝑌 ) ) )