Theorem curf11

Description: Value of the double evaluated 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 )
	curf1.x	|- ( ph -> X e. A )
	curf1.k	|- K = ( ( 1st ` G ) ` X )
	curf11.y	|- ( ph -> Y e. B )
Assertion	curf11	|- ( ph -> ( ( 1st ` K ) ` Y ) = ( X ( 1st ` F ) Y ) )

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		curf1.x	|- ( ph -> X e. A )
8		curf1.k	|- K = ( ( 1st ` G ) ` X )
9		curf11.y	|- ( ph -> Y e. B )
10		eqid	|- ( Hom ` D ) = ( Hom ` D )
11		eqid	|- ( Id ` C ) = ( Id ` C )
12	1 2 3 4 5 6 7 8 10 11	curf1	|- ( ph -> K = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. )
13	6	fvexi	|- B e. _V
14	13	mptex	|- ( y e. B |-> ( X ( 1st ` F ) y ) ) e. _V
15	13 13	mpoex	|- ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) e. _V
16	14 15	op1std	|- ( K = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` F ) y ) ) )
17	12 16	syl	|- ( ph -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` F ) y ) ) )
18		simpr	|- ( ( ph /\ y = Y ) -> y = Y )
19	18	oveq2d	|- ( ( ph /\ y = Y ) -> ( X ( 1st ` F ) y ) = ( X ( 1st ` F ) Y ) )
20		ovexd	|- ( ph -> ( X ( 1st ` F ) Y ) e. _V )
21	17 19 9 20	fvmptd	|- ( ph -> ( ( 1st ` K ) ` Y ) = ( X ( 1st ` F ) Y ) )