# 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}=⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}$
uncfval.c ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
uncfval.d ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
uncfval.f ${⊢}{\phi }\to {G}\in \left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)$
uncf1.a ${⊢}{A}={\mathrm{Base}}_{{C}}$
uncf1.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
uncf1.x ${⊢}{\phi }\to {X}\in {A}$
uncf1.y ${⊢}{\phi }\to {Y}\in {B}$
Assertion uncf1 ${⊢}{\phi }\to {X}{1}^{st}\left({F}\right){Y}={1}^{st}\left({1}^{st}\left({G}\right)\left({X}\right)\right)\left({Y}\right)$

### Proof

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