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 ) )

Metamath Proof Explorer

Theorem uncfcl

Proof