diagval

Description: Define the diagonal functor, which is the functor C --> ( D Func C ) whose object part is x e. C |-> ( y e. D |-> x ) . We can define this equationally as the currying of the first projection functor, and by expressing it this way we get a quick proof of functoriality. (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	diagval.l	$⊢ L = C Δ_{func} D$
	diagval.c	$⊢ φ \to C \in Cat$
	diagval.d	$⊢ φ \to D \in Cat$
Assertion	diagval	$⊢ φ \to L = ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D)$

Proof

Step	Hyp	Ref	Expression
1		diagval.l	$⊢ L = C Δ_{func} D$
2		diagval.c	$⊢ φ \to C \in Cat$
3		diagval.d	$⊢ φ \to D \in Cat$
4		df-diag	$⊢ Δ_{func} = (c \in Cat, d \in Cat ⟼ ⟨c, d⟩ {curry}_{F} (c {1^{st}}_{F} d))$
5	4	a1i	$⊢ φ \to Δ_{func} = (c \in Cat, d \in Cat ⟼ ⟨c, d⟩ {curry}_{F} (c {1^{st}}_{F} d))$
6		simprl	$⊢ (φ \land (c = C \land d = D)) \to c = C$
7		simprr	$⊢ (φ \land (c = C \land d = D)) \to d = D$
8	6 7	opeq12d	$⊢ (φ \land (c = C \land d = D)) \to ⟨c, d⟩ = ⟨C, D⟩$
9	6 7	oveq12d	$⊢ (φ \land (c = C \land d = D)) \to c {1^{st}}_{F} d = C {1^{st}}_{F} D$
10	8 9	oveq12d	$⊢ (φ \land (c = C \land d = D)) \to ⟨c, d⟩ {curry}_{F} (c {1^{st}}_{F} d) = ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D)$
11		ovexd	$⊢ φ \to ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D) \in V$
12	5 10 2 3 11	ovmpod	$⊢ φ \to C Δ_{func} D = ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D)$
13	1 12	eqtrid	$⊢ φ \to L = ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D)$

Metamath Proof Explorer

Theorem diagval

Proof