Metamath Proof Explorer


Theorem curf2

Description: Value of the curry functor at a morphism. (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𝐺 ) 𝑌 ) ‘ 𝐾 )
Assertion curf2 ( 𝜑𝐿 = ( 𝑧𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 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 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
14 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
15 1 2 3 4 5 6 13 14 7 8 curfval ( 𝜑𝐺 = ⟨ ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) ) ⟩ )
16 2 fvexi 𝐴 ∈ V
17 16 mptex ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) ∈ V
18 16 16 mpoex ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) ) ∈ V
19 17 18 op2ndd ( 𝐺 = ⟨ ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) ) ⟩ → ( 2nd𝐺 ) = ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) ) )
20 15 19 syl ( 𝜑 → ( 2nd𝐺 ) = ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) ) )
21 10 adantr ( ( 𝜑𝑥 = 𝑋 ) → 𝑌𝐴 )
22 ovex ( 𝑥 𝐻 𝑦 ) ∈ V
23 22 mptex ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) ∈ V
24 23 a1i ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) ∈ V )
25 11 adantr ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
26 simprl ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
27 simprr ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
28 26 27 oveq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
29 25 28 eleqtrrd ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝐾 ∈ ( 𝑥 𝐻 𝑦 ) )
30 6 fvexi 𝐵 ∈ V
31 30 mptex ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ∈ V
32 31 a1i ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ∈ V )
33 simplrl ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → 𝑥 = 𝑋 )
34 33 opeq1d ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑧 ⟩ )
35 simplrr ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → 𝑦 = 𝑌 )
36 35 opeq1d ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑌 , 𝑧 ⟩ )
37 34 36 oveq12d ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) = ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) )
38 simpr ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → 𝑔 = 𝐾 )
39 eqidd ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( 𝐼𝑧 ) = ( 𝐼𝑧 ) )
40 37 38 39 oveq123d ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) = ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) )
41 40 mpteq2dv ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) = ( 𝑧𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) )
42 29 32 41 fvmptdv2 ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) = ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) → ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) = ( 𝑧𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) )
43 9 21 24 42 ovmpodv ( 𝜑 → ( ( 2nd𝐺 ) = ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) ) → ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) = ( 𝑧𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) ) )
44 20 43 mpd ( 𝜑 → ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) = ( 𝑧𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) )
45 12 44 eqtrid ( 𝜑𝐿 = ( 𝑧𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼𝑧 ) ) ) )