Metamath Proof Explorer


Theorem curfpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses curfpropd.1 ( 𝜑 → ( Homf𝐴 ) = ( Homf𝐵 ) )
curfpropd.2 ( 𝜑 → ( compf𝐴 ) = ( compf𝐵 ) )
curfpropd.3 ( 𝜑 → ( Homf𝐶 ) = ( Homf𝐷 ) )
curfpropd.4 ( 𝜑 → ( compf𝐶 ) = ( compf𝐷 ) )
curfpropd.a ( 𝜑𝐴 ∈ Cat )
curfpropd.b ( 𝜑𝐵 ∈ Cat )
curfpropd.c ( 𝜑𝐶 ∈ Cat )
curfpropd.d ( 𝜑𝐷 ∈ Cat )
curfpropd.f ( 𝜑𝐹 ∈ ( ( 𝐴 ×c 𝐶 ) Func 𝐸 ) )
Assertion curfpropd ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ curryF 𝐹 ) = ( ⟨ 𝐵 , 𝐷 ⟩ curryF 𝐹 ) )

Proof

Step Hyp Ref Expression
1 curfpropd.1 ( 𝜑 → ( Homf𝐴 ) = ( Homf𝐵 ) )
2 curfpropd.2 ( 𝜑 → ( compf𝐴 ) = ( compf𝐵 ) )
3 curfpropd.3 ( 𝜑 → ( Homf𝐶 ) = ( Homf𝐷 ) )
4 curfpropd.4 ( 𝜑 → ( compf𝐶 ) = ( compf𝐷 ) )
5 curfpropd.a ( 𝜑𝐴 ∈ Cat )
6 curfpropd.b ( 𝜑𝐵 ∈ Cat )
7 curfpropd.c ( 𝜑𝐶 ∈ Cat )
8 curfpropd.d ( 𝜑𝐷 ∈ Cat )
9 curfpropd.f ( 𝜑𝐹 ∈ ( ( 𝐴 ×c 𝐶 ) Func 𝐸 ) )
10 1 homfeqbas ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
11 3 homfeqbas ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
12 11 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
13 12 mpteq1d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) )
14 12 adantr ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
15 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
16 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
17 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
18 3 ad2antrr ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( Homf𝐶 ) = ( Homf𝐷 ) )
19 simprl ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
20 simprr ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
21 15 16 17 18 19 20 homfeqval ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
22 1 2 5 6 cidpropd ( 𝜑 → ( Id ‘ 𝐴 ) = ( Id ‘ 𝐵 ) )
23 22 ad2antrr ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( Id ‘ 𝐴 ) = ( Id ‘ 𝐵 ) )
24 23 fveq1d ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) = ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) )
25 24 oveq1d ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) = ( ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) )
26 21 25 mpteq12dv ( ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) )
27 12 14 26 mpoeq123dva ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) )
28 13 27 opeq12d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) → ⟨ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ = ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
29 10 28 mpteq12dva ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) = ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
30 10 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
31 eqid ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
32 eqid ( Hom ‘ 𝐴 ) = ( Hom ‘ 𝐴 )
33 eqid ( Hom ‘ 𝐵 ) = ( Hom ‘ 𝐵 )
34 1 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( Homf𝐴 ) = ( Homf𝐵 ) )
35 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
36 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
37 31 32 33 34 35 36 homfeqval ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
38 11 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
39 3 4 7 8 cidpropd ( 𝜑 → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )
40 39 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )
41 40 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑧 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) )
42 41 oveq2d ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑧 ) ) = ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) )
43 38 42 mpteq12dva ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) )
44 37 43 mpteq12dva ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑧 ) ) ) ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
45 10 30 44 mpoeq123dva ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐴 ) , 𝑦 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑧 ) ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐵 ) , 𝑦 ∈ ( Base ‘ 𝐵 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) )
46 29 45 opeq12d ( 𝜑 → ⟨ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐴 ) , 𝑦 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑧 ) ) ) ) ) ⟩ = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐵 ) , 𝑦 ∈ ( Base ‘ 𝐵 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
47 eqid ( ⟨ 𝐴 , 𝐶 ⟩ curryF 𝐹 ) = ( ⟨ 𝐴 , 𝐶 ⟩ curryF 𝐹 )
48 eqid ( Id ‘ 𝐴 ) = ( Id ‘ 𝐴 )
49 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
50 47 31 5 7 9 15 16 48 32 49 curfval ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ curryF 𝐹 ) = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐴 ) , 𝑦 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
51 eqid ( ⟨ 𝐵 , 𝐷 ⟩ curryF 𝐹 ) = ( ⟨ 𝐵 , 𝐷 ⟩ curryF 𝐹 )
52 eqid ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
53 1 2 3 4 5 6 7 8 xpcpropd ( 𝜑 → ( 𝐴 ×c 𝐶 ) = ( 𝐵 ×c 𝐷 ) )
54 53 oveq1d ( 𝜑 → ( ( 𝐴 ×c 𝐶 ) Func 𝐸 ) = ( ( 𝐵 ×c 𝐷 ) Func 𝐸 ) )
55 9 54 eleqtrd ( 𝜑𝐹 ∈ ( ( 𝐵 ×c 𝐷 ) Func 𝐸 ) )
56 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
57 eqid ( Id ‘ 𝐵 ) = ( Id ‘ 𝐵 )
58 eqid ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
59 51 52 6 8 55 56 17 57 33 58 curfval ( 𝜑 → ( ⟨ 𝐵 , 𝐷 ⟩ curryF 𝐹 ) = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐵 ) , 𝑦 ∈ ( Base ‘ 𝐵 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
60 46 50 59 3eqtr4d ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ curryF 𝐹 ) = ( ⟨ 𝐵 , 𝐷 ⟩ curryF 𝐹 ) )