Theorem curf1fval

Description: Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	|- G = ( <. C , D >. curryF F )
	curfval.a	|- A = ( Base ` C )
	curfval.c	|- ( ph -> C e. Cat )
	curfval.d	|- ( ph -> D e. Cat )
	curfval.f	|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
	curfval.b	|- B = ( Base ` D )
	curfval.j	|- J = ( Hom ` D )
	curfval.1	|- .1. = ( Id ` C )
Assertion	curf1fval	|- ( ph -> ( 1st ` G ) = ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		curfval.g	|- G = ( <. C , D >. curryF F )
2		curfval.a	|- A = ( Base ` C )
3		curfval.c	|- ( ph -> C e. Cat )
4		curfval.d	|- ( ph -> D e. Cat )
5		curfval.f	|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
6		curfval.b	|- B = ( Base ` D )
7		curfval.j	|- J = ( Hom ` D )
8		curfval.1	|- .1. = ( Id ` C )
9		eqid	|- ( Hom ` C ) = ( Hom ` C )
10		eqid	|- ( Id ` D ) = ( Id ` D )
11	1 2 3 4 5 6 7 8 9 10	curfval	|- ( ph -> G = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) >. )
12	2	fvexi	|- A e. _V
13	12	mptex	|- ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) e. _V
14	12 12	mpoex	|- ( x e. A , y e. A |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) e. _V
15	13 14	op1std	|- ( G = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) >. -> ( 1st ` G ) = ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) )
16	11 15	syl	|- ( ph -> ( 1st ` G ) = ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) )