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 "> uncurryF G )
uncfval.c 
|- ( ph -> D e. Cat )
uncfval.d 
|- ( ph -> E e. Cat )
uncfval.f 
|- ( ph -> G e. ( C Func ( D FuncCat E ) ) )
Assertion uncfcl 
|- ( ph -> F e. ( ( C Xc. D ) Func E ) )

Proof

Step Hyp Ref Expression
1 uncfval.g 
 |-  F = ( <" C D E "> uncurryF G )
2 uncfval.c 
 |-  ( ph -> D e. Cat )
3 uncfval.d 
 |-  ( ph -> E e. Cat )
4 uncfval.f 
 |-  ( ph -> G e. ( C Func ( D FuncCat E ) ) )
5 1 2 3 4 uncfval 
 |-  ( ph -> F = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) )
6 eqid 
 |-  ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) = ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) )
7 eqid 
 |-  ( ( D FuncCat E ) Xc. D ) = ( ( D FuncCat E ) Xc. D )
8 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
9 funcrcl 
 |-  ( G e. ( C Func ( D FuncCat E ) ) -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
10 4 9 syl 
 |-  ( ph -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
11 10 simpld 
 |-  ( ph -> C e. Cat )
12 eqid 
 |-  ( C 1stF D ) = ( C 1stF D )
13 8 11 2 12 1stfcl 
 |-  ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) )
14 13 4 cofucl 
 |-  ( ph -> ( G o.func ( C 1stF D ) ) e. ( ( C Xc. D ) Func ( D FuncCat E ) ) )
15 eqid 
 |-  ( C 2ndF D ) = ( C 2ndF D )
16 8 11 2 15 2ndfcl 
 |-  ( ph -> ( C 2ndF D ) e. ( ( C Xc. D ) Func D ) )
17 6 7 14 16 prfcl 
 |-  ( ph -> ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) e. ( ( C Xc. D ) Func ( ( D FuncCat E ) Xc. D ) ) )
18 eqid 
 |-  ( D evalF E ) = ( D evalF E )
19 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
20 18 19 2 3 evlfcl 
 |-  ( ph -> ( D evalF E ) e. ( ( ( D FuncCat E ) Xc. D ) Func E ) )
21 17 20 cofucl 
 |-  ( ph -> ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) e. ( ( C Xc. D ) Func E ) )
22 5 21 eqeltrd 
 |-  ( ph -> F e. ( ( C Xc. D ) Func E ) )