Theorem 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	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
	diagval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diagval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	diagval	⊢ ( 𝜑 → 𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		diagval.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
2		diagval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		diagval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		df-diag	⊢ Δfunc = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ( ⟨ 𝑐 , 𝑑 ⟩ curryF ( 𝑐 1stF 𝑑 ) ) )
5	4	a1i	⊢ ( 𝜑 → Δfunc = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ( ⟨ 𝑐 , 𝑑 ⟩ curryF ( 𝑐 1stF 𝑑 ) ) ) )
6		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → 𝑐 = 𝐶 )
7		simprr	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → 𝑑 = 𝐷 )
8	6 7	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
9	6 7	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ( 𝑐 1stF 𝑑 ) = ( 𝐶 1stF 𝐷 ) )
10	8 9	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ( ⟨ 𝑐 , 𝑑 ⟩ curryF ( 𝑐 1stF 𝑑 ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) )
11		ovexd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ∈ V )
12	5 10 2 3 11	ovmpod	⊢ ( 𝜑 → ( 𝐶 Δfunc 𝐷 ) = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) )
13	1 12	syl5eq	⊢ ( 𝜑 → 𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) )