Metamath Proof Explorer


Theorem uncf1

Description: Value of the uncurry functor on an object. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfval.g F = ⟨“ CDE ”⟩ uncurry F G
uncfval.c φ D Cat
uncfval.d φ E Cat
uncfval.f φ G C Func D FuncCat E
uncf1.a A = Base C
uncf1.b B = Base D
uncf1.x φ X A
uncf1.y φ Y B
Assertion uncf1 φ X 1 st F Y = 1 st 1 st G X Y

Proof

Step Hyp Ref Expression
1 uncfval.g F = ⟨“ CDE ”⟩ uncurry F G
2 uncfval.c φ D Cat
3 uncfval.d φ E Cat
4 uncfval.f φ G C Func D FuncCat E
5 uncf1.a A = Base C
6 uncf1.b B = Base D
7 uncf1.x φ X A
8 uncf1.y φ Y B
9 1 2 3 4 uncfval φ F = D eval F E func G func C 1 st F D ⟨,⟩ F C 2 nd F D
10 9 fveq2d φ 1 st F = 1 st D eval F E func G func C 1 st F D ⟨,⟩ F C 2 nd F D
11 10 oveqd φ X 1 st F Y = X 1 st D eval F E func G func C 1 st F D ⟨,⟩ F C 2 nd F D Y
12 df-ov X 1 st D eval F E func G func C 1 st F D ⟨,⟩ F C 2 nd F D Y = 1 st D eval F E func G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y
13 eqid C × c D = C × c D
14 13 5 6 xpcbas A × B = Base C × c D
15 eqid G func C 1 st F D ⟨,⟩ F C 2 nd F D = G func C 1 st F D ⟨,⟩ F C 2 nd F D
16 eqid D FuncCat E × c D = D FuncCat E × c D
17 funcrcl G C Func D FuncCat E C Cat D FuncCat E Cat
18 4 17 syl φ C Cat D FuncCat E Cat
19 18 simpld φ C Cat
20 eqid C 1 st F D = C 1 st F D
21 13 19 2 20 1stfcl φ C 1 st F D C × c D Func C
22 21 4 cofucl φ G func C 1 st F D C × c D Func D FuncCat E
23 eqid C 2 nd F D = C 2 nd F D
24 13 19 2 23 2ndfcl φ C 2 nd F D C × c D Func D
25 15 16 22 24 prfcl φ G func C 1 st F D ⟨,⟩ F C 2 nd F D C × c D Func D FuncCat E × c D
26 eqid D eval F E = D eval F E
27 eqid D FuncCat E = D FuncCat E
28 26 27 2 3 evlfcl φ D eval F E D FuncCat E × c D Func E
29 7 8 opelxpd φ X Y A × B
30 14 25 28 29 cofu1 φ 1 st D eval F E func G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y = 1 st D eval F E 1 st G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y
31 12 30 syl5eq φ X 1 st D eval F E func G func C 1 st F D ⟨,⟩ F C 2 nd F D Y = 1 st D eval F E 1 st G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y
32 eqid Hom C × c D = Hom C × c D
33 15 14 32 22 24 29 prf1 φ 1 st G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y = 1 st G func C 1 st F D X Y 1 st C 2 nd F D X Y
34 14 21 4 29 cofu1 φ 1 st G func C 1 st F D X Y = 1 st G 1 st C 1 st F D X Y
35 13 14 32 19 2 20 29 1stf1 φ 1 st C 1 st F D X Y = 1 st X Y
36 op1stg X A Y B 1 st X Y = X
37 7 8 36 syl2anc φ 1 st X Y = X
38 35 37 eqtrd φ 1 st C 1 st F D X Y = X
39 38 fveq2d φ 1 st G 1 st C 1 st F D X Y = 1 st G X
40 34 39 eqtrd φ 1 st G func C 1 st F D X Y = 1 st G X
41 13 14 32 19 2 23 29 2ndf1 φ 1 st C 2 nd F D X Y = 2 nd X Y
42 op2ndg X A Y B 2 nd X Y = Y
43 7 8 42 syl2anc φ 2 nd X Y = Y
44 41 43 eqtrd φ 1 st C 2 nd F D X Y = Y
45 40 44 opeq12d φ 1 st G func C 1 st F D X Y 1 st C 2 nd F D X Y = 1 st G X Y
46 33 45 eqtrd φ 1 st G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y = 1 st G X Y
47 46 fveq2d φ 1 st D eval F E 1 st G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y = 1 st D eval F E 1 st G X Y
48 df-ov 1 st G X 1 st D eval F E Y = 1 st D eval F E 1 st G X Y
49 47 48 syl6eqr φ 1 st D eval F E 1 st G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y = 1 st G X 1 st D eval F E Y
50 27 fucbas D Func E = Base D FuncCat E
51 relfunc Rel C Func D FuncCat E
52 1st2ndbr Rel C Func D FuncCat E G C Func D FuncCat E 1 st G C Func D FuncCat E 2 nd G
53 51 4 52 sylancr φ 1 st G C Func D FuncCat E 2 nd G
54 5 50 53 funcf1 φ 1 st G : A D Func E
55 54 7 ffvelrnd φ 1 st G X D Func E
56 26 2 3 6 55 8 evlf1 φ 1 st G X 1 st D eval F E Y = 1 st 1 st G X Y
57 49 56 eqtrd φ 1 st D eval F E 1 st G func C 1 st F D ⟨,⟩ F C 2 nd F D X Y = 1 st 1 st G X Y
58 11 31 57 3eqtrd φ X 1 st F Y = 1 st 1 st G X Y