This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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