# Metamath Proof Explorer

## Theorem uncfcurf

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

Ref Expression
Hypotheses uncfcurf.g $⊢ G = C D curry F F$
uncfcurf.c $⊢ φ → C ∈ Cat$
uncfcurf.d $⊢ φ → D ∈ Cat$
uncfcurf.f $⊢ φ → F ∈ C × c D Func E$
Assertion uncfcurf $⊢ φ → ⟨“ CDE ”⟩ uncurry F G = F$

### Proof

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