Metamath Proof Explorer


Theorem curf1fval

Description: Value of the object part of the curry functor. (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 ‘ 𝐷 )
curfval.j 𝐽 = ( Hom ‘ 𝐷 )
curfval.1 1 = ( Id ‘ 𝐶 )
Assertion curf1fval ( 𝜑 → ( 1st𝐺 ) = ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 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 curfval.j 𝐽 = ( Hom ‘ 𝐷 )
8 curfval.1 1 = ( Id ‘ 𝐶 )
9 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10 eqid ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
11 1 2 3 4 5 6 7 8 9 10 curfval ( 𝜑𝐺 = ⟨ ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
12 2 fvexi 𝐴 ∈ V
13 12 mptex ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) ∈ V
14 12 12 mpoex ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ∈ V
15 13 14 op1std ( 𝐺 = ⟨ ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥𝐴 , 𝑦𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ → ( 1st𝐺 ) = ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
16 11 15 syl ( 𝜑 → ( 1st𝐺 ) = ( 𝑥𝐴 ↦ ⟨ ( 𝑦𝐵 ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦𝐵 , 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )