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 = ⟨“ CDE ”⟩ uncurry F G
uncfval.c ⊢ φ → D ∈ Cat
uncfval.d ⊢ φ → E ∈ Cat
uncfval.f ⊢ φ → G ∈ C Func D FuncCat E
Assertion uncfcl ⊢ φ → F ∈ C × c D Func E

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 1 2 3 4 uncfval ⊢ φ → F = D eval F E ∘ func G ∘ func C 1 st F D ⟨,⟩ F C 2 nd F D
6 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
7 eqid ⊢ D FuncCat E × c D = D FuncCat E × c D
8 eqid ⊢ C × c D = C × c D
9 funcrcl ⊢ G ∈ C Func D FuncCat E → C ∈ Cat ∧ D FuncCat E ∈ Cat
10 4 9 syl ⊢ φ → C ∈ Cat ∧ D FuncCat E ∈ Cat
11 10 simpld ⊢ φ → C ∈ Cat
12 eqid ⊢ C 1 st F D = C 1 st F D
13 8 11 2 12 1stfcl ⊢ φ → C 1 st F D ∈ C × c D Func C
14 13 4 cofucl ⊢ φ → G ∘ func C 1 st F D ∈ C × c D Func D FuncCat E
15 eqid ⊢ C 2 nd F D = C 2 nd F D
16 8 11 2 15 2ndfcl ⊢ φ → C 2 nd F D ∈ C × c D Func D
17 6 7 14 16 prfcl ⊢ φ → G ∘ func C 1 st F D ⟨,⟩ F C 2 nd F D ∈ C × c D Func D FuncCat E × c D
18 eqid ⊢ D eval F E = D eval F E
19 eqid ⊢ D FuncCat E = D FuncCat E
20 18 19 2 3 evlfcl ⊢ φ → D eval F E ∈ D FuncCat E × c D Func E
21 17 20 cofucl ⊢ φ → D eval F E ∘ func G ∘ func C 1 st F D ⟨,⟩ F C 2 nd F D ∈ C × c D Func E
22 5 21 eqeltrd ⊢ φ → F ∈ C × c D Func E