Metamath Proof Explorer


Theorem uncfcurf

Description: Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfcurf.g 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
uncfcurf.c ( 𝜑𝐶 ∈ Cat )
uncfcurf.d ( 𝜑𝐷 ∈ Cat )
uncfcurf.f ( 𝜑𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
Assertion uncfcurf ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 uncfcurf.g 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
2 uncfcurf.c ( 𝜑𝐶 ∈ Cat )
3 uncfcurf.d ( 𝜑𝐷 ∈ Cat )
4 uncfcurf.f ( 𝜑𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
5 eqid ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 )
6 3 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐷 ∈ Cat )
7 funcrcl ( 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) → ( ( 𝐶 ×c 𝐷 ) ∈ Cat ∧ 𝐸 ∈ Cat ) )
8 4 7 syl ( 𝜑 → ( ( 𝐶 ×c 𝐷 ) ∈ Cat ∧ 𝐸 ∈ Cat ) )
9 8 simprd ( 𝜑𝐸 ∈ Cat )
10 9 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐸 ∈ Cat )
11 eqid ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
12 1 11 2 3 4 curfcl ( 𝜑𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
13 12 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
14 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
15 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
16 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
17 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
18 5 6 10 13 14 15 16 17 uncf1 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑦 ) = ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) )
19 2 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐶 ∈ Cat )
20 4 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
21 eqid ( ( 1st𝐺 ) ‘ 𝑥 ) = ( ( 1st𝐺 ) ‘ 𝑥 )
22 1 14 19 6 20 15 16 21 17 curf11 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) = ( 𝑥 ( 1st𝐹 ) 𝑦 ) )
23 18 22 eqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑦 ) = ( 𝑥 ( 1st𝐹 ) 𝑦 ) )
24 23 ralrimivva ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑦 ) = ( 𝑥 ( 1st𝐹 ) 𝑦 ) )
25 eqid ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
26 25 14 15 xpcbas ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ ( 𝐶 ×c 𝐷 ) )
27 eqid ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
28 relfunc Rel ( ( 𝐶 ×c 𝐷 ) Func 𝐸 )
29 5 3 9 12 uncfcl ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
30 1st2ndbr ( ( Rel ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ∧ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ) → ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) )
31 28 29 30 sylancr ( 𝜑 → ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) )
32 26 27 31 funcf1 ( 𝜑 → ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐸 ) )
33 32 ffnd ( 𝜑 → ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
34 1st2ndbr ( ( Rel ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ∧ 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ) → ( 1st𝐹 ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd𝐹 ) )
35 28 4 34 sylancr ( 𝜑 → ( 1st𝐹 ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd𝐹 ) )
36 26 27 35 funcf1 ( 𝜑 → ( 1st𝐹 ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐸 ) )
37 36 ffnd ( 𝜑 → ( 1st𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
38 eqfnov2 ( ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ ( 1st𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) = ( 1st𝐹 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑦 ) = ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) )
39 33 37 38 syl2anc ( 𝜑 → ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) = ( 1st𝐹 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑦 ) = ( 𝑥 ( 1st𝐹 ) 𝑦 ) ) )
40 24 39 mpbird ( 𝜑 → ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) = ( 1st𝐹 ) )
41 3 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐷 ∈ Cat )
42 9 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐸 ∈ Cat )
43 12 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
44 16 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
45 44 adantr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
46 17 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
47 46 adantr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
48 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
49 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
50 simprl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
51 50 adantr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
52 simprr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐷 ) )
53 52 adantr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐷 ) )
54 simprl ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
55 simprr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) )
56 5 41 42 43 14 15 45 47 48 49 51 53 54 55 uncf2 ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( ( ( ( 𝑥 ( 2nd𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( 𝑦 ( 2nd ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) ) )
57 2 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐶 ∈ Cat )
58 4 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
59 1 14 57 41 58 15 45 21 47 curf11 ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) = ( 𝑥 ( 1st𝐹 ) 𝑦 ) )
60 df-ov ( 𝑥 ( 1st𝐹 ) 𝑦 ) = ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
61 59 60 syl6eq ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) = ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
62 1 14 57 41 58 15 45 21 53 curf11 ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) = ( 𝑥 ( 1st𝐹 ) 𝑤 ) )
63 df-ov ( 𝑥 ( 1st𝐹 ) 𝑤 ) = ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ )
64 62 63 syl6eq ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) = ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) )
65 61 64 opeq12d ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ = ⟨ ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) ⟩ )
66 eqid ( ( 1st𝐺 ) ‘ 𝑧 ) = ( ( 1st𝐺 ) ‘ 𝑧 )
67 1 14 57 41 58 15 51 66 53 curf11 ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) = ( 𝑧 ( 1st𝐹 ) 𝑤 ) )
68 df-ov ( 𝑧 ( 1st𝐹 ) 𝑤 ) = ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ )
69 67 68 syl6eq ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) = ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
70 65 69 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
71 eqid ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
72 eqid ( ( 𝑥 ( 2nd𝐺 ) 𝑧 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2nd𝐺 ) 𝑧 ) ‘ 𝑓 )
73 1 14 57 41 58 15 48 71 45 51 54 72 53 curf2val ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( 𝑥 ( 2nd𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) )
74 df-ov ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
75 73 74 syl6eq ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( 𝑥 ( 2nd𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) )
76 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
77 1 14 57 41 58 15 45 21 47 49 76 53 55 curf12 ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑦 ( 2nd ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) 𝑔 ) )
78 df-ov ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) 𝑔 ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ )
79 77 78 syl6eq ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑦 ( 2nd ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) )
80 70 75 79 oveq123d ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( ( 𝑥 ( 2nd𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( 𝑦 ( 2nd ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) )
81 eqid ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) )
82 eqid ( comp ‘ ( 𝐶 ×c 𝐷 ) ) = ( comp ‘ ( 𝐶 ×c 𝐷 ) )
83 eqid ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
84 35 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( 1st𝐹 ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd𝐹 ) )
85 84 adantr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 1st𝐹 ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd𝐹 ) )
86 opelxpi ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
87 86 ad2antlr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
88 87 adantr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
89 45 53 opelxpd ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑥 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
90 opelxpi ( ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
91 90 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
92 91 adantr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
93 14 48 76 57 45 catidcl ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
94 93 55 opelxpd ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
95 25 14 15 48 49 45 47 45 53 81 xpchom2 ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑤 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
96 94 95 eleqtrrd ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ∈ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑤 ⟩ ) )
97 15 49 71 41 53 catidcl ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ∈ ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) )
98 54 97 opelxpd ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
99 25 14 15 48 49 45 53 51 53 81 xpchom2 ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑥 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
100 98 99 eleqtrrd ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ∈ ( ⟨ 𝑥 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) )
101 26 81 82 83 85 88 89 92 96 100 funcco ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) = ( ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) )
102 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
103 eqid ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
104 25 14 15 48 49 45 47 45 53 102 103 82 51 53 93 55 54 97 xpcco2 ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) = ⟨ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ )
105 104 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ ) )
106 df-ov ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ )
107 105 106 syl6eqr ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) = ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) )
108 14 48 76 57 45 102 51 54 catrid ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = 𝑓 )
109 15 49 71 41 47 103 53 55 catlid ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) = 𝑔 )
110 108 109 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
111 107 110 eqtrd ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
112 80 101 111 3eqtr2d ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( ( 𝑥 ( 2nd𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( 𝑦 ( 2nd ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
113 56 112 eqtrd ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
114 113 ralrimivva ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
115 eqid ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
116 31 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) )
117 26 81 115 116 87 91 funcf2 ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟶ ( ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
118 25 14 15 48 49 44 46 50 52 81 xpchom2 ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
119 118 feq2d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟶ ( ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ⟶ ( ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
120 117 119 mpbid ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ⟶ ( ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
121 120 ffnd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) Fn ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
122 26 81 115 84 87 91 funcf2 ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟶ ( ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
123 118 feq2d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟶ ( ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ⟶ ( ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
124 122 123 mpbid ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ⟶ ( ( ( 1st𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1st𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
125 124 ffnd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) Fn ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
126 eqfnov2 ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) Fn ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) Fn ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) ) )
127 121 125 126 syl2anc ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) ) )
128 114 127 mpbird ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
129 128 ralrimivva ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
130 129 ralrimivva ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
131 oveq2 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) )
132 oveq2 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑢 ( 2nd𝐹 ) 𝑣 ) = ( 𝑢 ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
133 131 132 eqeq12d ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2nd𝐹 ) 𝑣 ) ↔ ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( 𝑢 ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
134 133 ralxp ( ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2nd𝐹 ) 𝑣 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( 𝑢 ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
135 oveq1 ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) )
136 oveq1 ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑢 ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
137 135 136 eqeq12d ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( 𝑢 ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
138 137 2ralbidv ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( 𝑢 ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
139 134 138 syl5bb ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2nd𝐹 ) 𝑣 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
140 139 ralxp ( ∀ 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2nd𝐹 ) 𝑣 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
141 130 140 sylibr ( 𝜑 → ∀ 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2nd𝐹 ) 𝑣 ) )
142 26 31 funcfn2 ( 𝜑 → ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) )
143 26 35 funcfn2 ( 𝜑 → ( 2nd𝐹 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) )
144 eqfnov2 ( ( ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 2nd𝐹 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) = ( 2nd𝐹 ) ↔ ∀ 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2nd𝐹 ) 𝑣 ) ) )
145 142 143 144 syl2anc ( 𝜑 → ( ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) = ( 2nd𝐹 ) ↔ ∀ 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2nd𝐹 ) 𝑣 ) ) )
146 141 145 mpbird ( 𝜑 → ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) = ( 2nd𝐹 ) )
147 40 146 opeq12d ( 𝜑 → ⟨ ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) , ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟩ = ⟨ ( 1st𝐹 ) , ( 2nd𝐹 ) ⟩ )
148 1st2nd ( ( Rel ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ∧ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ) → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) = ⟨ ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) , ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟩ )
149 28 29 148 sylancr ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) = ⟨ ( 1st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) , ( 2nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) ) ⟩ )
150 1st2nd ( ( Rel ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ∧ 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ) → 𝐹 = ⟨ ( 1st𝐹 ) , ( 2nd𝐹 ) ⟩ )
151 28 4 150 sylancr ( 𝜑𝐹 = ⟨ ( 1st𝐹 ) , ( 2nd𝐹 ) ⟩ )
152 147 149 151 3eqtr4d ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) = 𝐹 )