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

Metamath Proof Explorer

Theorem curf2val

Description: Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curf2.g ⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
curf2.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
curf2.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
curf2.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
curf2.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
curf2.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
curf2.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
curf2.i ⊢ 𝐼 = ( Id ‘ 𝐷 )
curf2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
curf2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
curf2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
curf2.l ⊢ 𝐿 = ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 )
curf2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion curf2val ( 𝜑 → ( 𝐿 ‘ 𝑍 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) ( 𝐼 ‘ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 curf2.g ⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
2 curf2.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
3 curf2.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 curf2.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
5 curf2.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
6 curf2.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
7 curf2.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
8 curf2.i ⊢ 𝐼 = ( Id ‘ 𝐷 )
9 curf2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
10 curf2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
11 curf2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
12 curf2.l ⊢ 𝐿 = ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 )
13 curf2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
14 1 2 3 4 5 6 7 8 9 10 11 12 curf2 ⊢ ( 𝜑 → 𝐿 = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝑧 = 𝑍 )
16 15 opeq2d ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ⟨ 𝑋 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑍 ⟩ )
17 15 opeq2d ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ⟨ 𝑌 , 𝑧 ⟩ = ⟨ 𝑌 , 𝑍 ⟩ )
18 16 17 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) = ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) )
19 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝐾 = 𝐾 )
20 15 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑍 ) )
21 18 19 20 oveq123d ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) ( 𝐼 ‘ 𝑍 ) ) )
22 ovexd ⊢ ( 𝜑 → ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) ( 𝐼 ‘ 𝑍 ) ) ∈ V )
23 14 21 13 22 fvmptd ⊢ ( 𝜑 → ( 𝐿 ‘ 𝑍 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) ( 𝐼 ‘ 𝑍 ) ) )