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

Metamath Proof Explorer

Theorem curf12

Description: The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses curfval.g ⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
curfval.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
curfval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
curfval.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
curfval.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
curfval.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
curf1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
curf1.k ⊢ 𝐾 = ( ( 1st ‘ 𝐺 ) ‘ 𝑋 )
curf11.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
curf12.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
curf12.1 ⊢ 1 = ( Id ‘ 𝐶 )
curf12.y ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
curf12.g ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑌 𝐽 𝑍 ) )
Assertion curf12 ( 𝜑 → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) )

Proof

Step Hyp Ref Expression
1 curfval.g ⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
2 curfval.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
3 curfval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 curfval.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
5 curfval.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
6 curfval.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
7 curf1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8 curf1.k ⊢ 𝐾 = ( ( 1st ‘ 𝐺 ) ‘ 𝑋 )
9 curf11.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10 curf12.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
11 curf12.1 ⊢ 1 = ( Id ‘ 𝐶 )
12 curf12.y ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
13 curf12.g ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑌 𝐽 𝑍 ) )
14 1 2 3 4 5 6 7 8 10 11 curf1 ⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
15 6 fvexi ⊢ 𝐵 ∈ V
16 15 mptex ⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1st ‘ 𝐹 ) 𝑦 ) ) ∈ V
17 15 15 mpoex ⊢ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ∈ V
18 16 17 op2ndd ⊢ ( 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ → ( 2nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
19 14 18 syl ⊢ ( 𝜑 → ( 2nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
20 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ 𝐵 )
21 ovex ⊢ ( 𝑦 𝐽 𝑧 ) ∈ V
22 21 mptex ⊢ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ∈ V
23 22 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ∈ V )
24 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → 𝐻 ∈ ( 𝑌 𝐽 𝑍 ) )
25 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → 𝑦 = 𝑌 )
26 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
27 25 26 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → ( 𝑦 𝐽 𝑧 ) = ( 𝑌 𝐽 𝑍 ) )
28 24 27 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → 𝐻 ∈ ( 𝑦 𝐽 𝑧 ) )
29 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ∈ V )
30 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → 𝑦 = 𝑌 )
31 30 opeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ⟨ 𝑋 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
32 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → 𝑧 = 𝑍 )
33 32 opeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ⟨ 𝑋 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑍 ⟩ )
34 31 33 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) )
35 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ( 1 ‘ 𝑋 ) = ( 1 ‘ 𝑋 ) )
36 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → 𝑔 = 𝐻 )
37 34 35 36 oveq123d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) )
38 28 29 37 fvmptdv2 ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) = ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) ) )
39 9 20 23 38 ovmpodv ⊢ ( 𝜑 → ( ( 2nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) ) )
40 19 39 mpd ⊢ ( 𝜑 → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) )