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 𝐹 ) )