Metamath Proof Explorer

Theorem uncf1

Description: Value of the uncurry functor on an object. (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 ) ) )
uncf1.a 
|- A = ( Base ` C )
uncf1.b 
|- B = ( Base ` D )
uncf1.x 
|- ( ph -> X e. A )
uncf1.y 
|- ( ph -> Y e. B )
Assertion uncf1 
|- ( ph -> ( X ( 1st ` F ) Y ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) )

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 uncf1.a 
 |-  A = ( Base ` C )
6 uncf1.b 
 |-  B = ( Base ` D )
7 uncf1.x 
 |-  ( ph -> X e. A )
8 uncf1.y 
 |-  ( ph -> Y e. B )
9 1 2 3 4 uncfval 
 |-  ( ph -> F = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) )
10 9 fveq2d 
 |-  ( ph -> ( 1st ` F ) = ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) )
11 10 oveqd 
 |-  ( ph -> ( X ( 1st ` F ) Y ) = ( X ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) Y ) )
12 df-ov 
 |-  ( X ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) Y ) = ( ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) ` <. X , Y >. )
13 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
14 13 5 6 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
15 eqid 
 |-  ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) = ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) )
16 eqid 
 |-  ( ( D FuncCat E ) Xc. D ) = ( ( D FuncCat E ) Xc. D )
17 funcrcl 
 |-  ( G e. ( C Func ( D FuncCat E ) ) -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
18 4 17 syl 
 |-  ( ph -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
19 18 simpld 
 |-  ( ph -> C e. Cat )
20 eqid 
 |-  ( C 1stF D ) = ( C 1stF D )
21 13 19 2 20 1stfcl 
 |-  ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) )
22 21 4 cofucl 
 |-  ( ph -> ( G o.func ( C 1stF D ) ) e. ( ( C Xc. D ) Func ( D FuncCat E ) ) )
23 eqid 
 |-  ( C 2ndF D ) = ( C 2ndF D )
24 13 19 2 23 2ndfcl 
 |-  ( ph -> ( C 2ndF D ) e. ( ( C Xc. D ) Func D ) )
25 15 16 22 24 prfcl 
 |-  ( ph -> ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) e. ( ( C Xc. D ) Func ( ( D FuncCat E ) Xc. D ) ) )
26 eqid 
 |-  ( D evalF E ) = ( D evalF E )
27 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
28 26 27 2 3 evlfcl 
 |-  ( ph -> ( D evalF E ) e. ( ( ( D FuncCat E ) Xc. D ) Func E ) )
29 7 8 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( A X. B ) )
30 14 25 28 29 cofu1 
 |-  ( ph -> ( ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) ` <. X , Y >. ) = ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) )
31 12 30 eqtrid 
 |-  ( ph -> ( X ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) Y ) = ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) )
32 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
33 15 14 32 22 24 29 prf1 
 |-  ( ph -> ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) = <. ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) , ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) >. )
34 14 21 4 29 cofu1 
 |-  ( ph -> ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` G ) ` ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ) )
35 13 14 32 19 2 20 29 1stf1 
 |-  ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) = ( 1st ` <. X , Y >. ) )
36 op1stg 
 |-  ( ( X e. A /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
37 7 8 36 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
38 35 37 eqtrd 
 |-  ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) = X )
39 38 fveq2d 
 |-  ( ph -> ( ( 1st ` G ) ` ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ) = ( ( 1st ` G ) ` X ) )
40 34 39 eqtrd 
 |-  ( ph -> ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` G ) ` X ) )
41 13 14 32 19 2 23 29 2ndf1 
 |-  ( ph -> ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) = ( 2nd ` <. X , Y >. ) )
42 op2ndg 
 |-  ( ( X e. A /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
43 7 8 42 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
44 41 43 eqtrd 
 |-  ( ph -> ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) = Y )
45 40 44 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) , ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) >. = <. ( ( 1st ` G ) ` X ) , Y >. )
46 33 45 eqtrd 
 |-  ( ph -> ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) = <. ( ( 1st ` G ) ` X ) , Y >. )
47 46 fveq2d 
 |-  ( ph -> ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) = ( ( 1st ` ( D evalF E ) ) ` <. ( ( 1st ` G ) ` X ) , Y >. ) )
48 df-ov 
 |-  ( ( ( 1st ` G ) ` X ) ( 1st ` ( D evalF E ) ) Y ) = ( ( 1st ` ( D evalF E ) ) ` <. ( ( 1st ` G ) ` X ) , Y >. )
49 47 48 eqtr4di 
 |-  ( ph -> ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) = ( ( ( 1st ` G ) ` X ) ( 1st ` ( D evalF E ) ) Y ) )
50 27 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
51 relfunc 
 |-  Rel ( C Func ( D FuncCat E ) )
52 1st2ndbr 
 |-  ( ( Rel ( C Func ( D FuncCat E ) ) /\ G e. ( C Func ( D FuncCat E ) ) ) -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
53 51 4 52 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
54 5 50 53 funcf1 
 |-  ( ph -> ( 1st ` G ) : A --> ( D Func E ) )
55 54 7 ffvelrnd 
 |-  ( ph -> ( ( 1st ` G ) ` X ) e. ( D Func E ) )
56 26 2 3 6 55 8 evlf1 
 |-  ( ph -> ( ( ( 1st ` G ) ` X ) ( 1st ` ( D evalF E ) ) Y ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) )
57 49 56 eqtrd 
 |-  ( ph -> ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) )
58 11 31 57 3eqtrd 
 |-  ( ph -> ( X ( 1st ` F ) Y ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) )