# Metamath Proof Explorer

## Theorem uncfcl

Description: The uncurry operation takes a functor F : C --> ( D --> E ) to a functor uncurryF ( F ) : C X. D --> E . (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)$
Assertion uncfcl ${⊢}{\phi }\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\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 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)$
6 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)$
7 eqid ${⊢}\left({D}\mathrm{FuncCat}{E}\right){×}_{c}{D}=\left({D}\mathrm{FuncCat}{E}\right){×}_{c}{D}$
8 eqid ${⊢}{C}{×}_{c}{D}={C}{×}_{c}{D}$
9 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)$
10 4 9 syl ${⊢}{\phi }\to \left({C}\in \mathrm{Cat}\wedge {D}\mathrm{FuncCat}{E}\in \mathrm{Cat}\right)$
11 10 simpld ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
12 eqid ${⊢}{C}{{1}^{st}}_{F}{D}={C}{{1}^{st}}_{F}{D}$
13 8 11 2 12 1stfcl ${⊢}{\phi }\to {C}{{1}^{st}}_{F}{D}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{C}\right)$
14 13 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)$
15 eqid ${⊢}{C}{{2}^{nd}}_{F}{D}={C}{{2}^{nd}}_{F}{D}$
16 8 11 2 15 2ndfcl ${⊢}{\phi }\to {C}{{2}^{nd}}_{F}{D}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{D}\right)$
17 6 7 14 16 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)$
18 eqid ${⊢}{D}{eval}_{F}{E}={D}{eval}_{F}{E}$
19 eqid ${⊢}{D}\mathrm{FuncCat}{E}={D}\mathrm{FuncCat}{E}$
20 18 19 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)$
21 17 20 cofucl ${⊢}{\phi }\to \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)\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
22 5 21 eqeltrd ${⊢}{\phi }\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$