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 Δ_{func} D$
	diag2.a	$⊢ A = {Base}_{C}$
	diag2.b	$⊢ B = {Base}_{D}$
	diag2.h	$⊢ H = Hom (C)$
	diag2.c	$⊢ φ \to C \in Cat$
	diag2.d	$⊢ φ \to D \in Cat$
	diag2.x	$⊢ φ \to X \in A$
	diag2.y	$⊢ φ \to Y \in A$
	diag2.f	$⊢ φ \to F \in (X H Y)$
	diag2cl.h	$⊢ N = D Nat C$
Assertion	diag2cl	$⊢ φ \to B \times \{F\} \in (1^{st} (L) (X) N 1^{st} (L) (Y))$

Proof

Step	Hyp	Ref	Expression
1		diag2.l	$⊢ L = C Δ_{func} D$
2		diag2.a	$⊢ A = {Base}_{C}$
3		diag2.b	$⊢ B = {Base}_{D}$
4		diag2.h	$⊢ H = Hom (C)$
5		diag2.c	$⊢ φ \to C \in Cat$
6		diag2.d	$⊢ φ \to D \in Cat$
7		diag2.x	$⊢ φ \to X \in A$
8		diag2.y	$⊢ φ \to Y \in A$
9		diag2.f	$⊢ φ \to F \in (X H Y)$
10		diag2cl.h	$⊢ N = D Nat C$
11	1 2 3 4 5 6 7 8 9	diag2	$⊢ φ \to (X 2^{nd} (L) Y) (F) = B \times \{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	$⊢ φ \to L \in (C Func (D FuncCat C))$
16		1st2ndbr	$⊢ (Rel (C Func (D FuncCat C)) \land L \in (C Func (D FuncCat C))) \to 1^{st} (L) (C Func (D FuncCat C)) 2^{nd} (L)$
17	14 15 16	sylancr	$⊢ φ \to 1^{st} (L) (C Func (D FuncCat C)) 2^{nd} (L)$
18	2 4 13 17 7 8	funcf2	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y ⟶ 1^{st} (L) (X) N 1^{st} (L) (Y)$
19	18 9	ffvelrnd	$⊢ φ \to (X 2^{nd} (L) Y) (F) \in (1^{st} (L) (X) N 1^{st} (L) (Y))$
20	11 19	eqeltrrd	$⊢ φ \to B \times \{F\} \in (1^{st} (L) (X) N 1^{st} (L) (Y))$

Metamath Proof Explorer

Theorem diag2cl

Proof