This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) )