Metamath Proof Explorer

Theorem diag11

Description: Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses diagval.l 
|- L = ( C DiagFunc D )
diagval.c 
|- ( ph -> C e. Cat )
diagval.d 
|- ( ph -> D e. Cat )
diag11.a 
|- A = ( Base ` C )
diag11.c 
|- ( ph -> X e. A )
diag11.k 
|- K = ( ( 1st ` L ) ` X )
diag11.b 
|- B = ( Base ` D )
diag11.y 
|- ( ph -> Y e. B )
Assertion diag11 
|- ( ph -> ( ( 1st ` K ) ` Y ) = X )

Proof

Step Hyp Ref Expression
1 diagval.l 
 |-  L = ( C DiagFunc D )
2 diagval.c 
 |-  ( ph -> C e. Cat )
3 diagval.d 
 |-  ( ph -> D e. Cat )
4 diag11.a 
 |-  A = ( Base ` C )
5 diag11.c 
 |-  ( ph -> X e. A )
6 diag11.k 
 |-  K = ( ( 1st ` L ) ` X )
7 diag11.b 
 |-  B = ( Base ` D )
8 diag11.y 
 |-  ( ph -> Y e. B )
9 1 2 3 diagval 
 |-  ( ph -> L = ( <. C , D >. curryF ( C 1stF D ) ) )
10 9 fveq2d 
 |-  ( ph -> ( 1st ` L ) = ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) )
11 10 fveq1d 
 |-  ( ph -> ( ( 1st ` L ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) )
12 6 11 syl5eq 
 |-  ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) )
13 12 fveq2d 
 |-  ( ph -> ( 1st ` K ) = ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) )
14 13 fveq1d 
 |-  ( ph -> ( ( 1st ` K ) ` Y ) = ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) ` Y ) )
15 eqid 
 |-  ( <. C , D >. curryF ( C 1stF D ) ) = ( <. C , D >. curryF ( C 1stF D ) )
16 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
17 eqid 
 |-  ( C 1stF D ) = ( C 1stF D )
18 16 2 3 17 1stfcl 
 |-  ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) )
19 eqid 
 |-  ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X )
20 15 4 2 3 18 7 5 19 8 curf11 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) ` Y ) = ( X ( 1st ` ( C 1stF D ) ) Y ) )
21 df-ov 
 |-  ( X ( 1st ` ( C 1stF D ) ) Y ) = ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. )
22 16 4 7 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
23 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
24 5 8 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( A X. B ) )
25 16 22 23 2 3 17 24 1stf1 
 |-  ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) = ( 1st ` <. X , Y >. ) )
26 21 25 syl5eq 
 |-  ( ph -> ( X ( 1st ` ( C 1stF D ) ) Y ) = ( 1st ` <. X , Y >. ) )
27 op1stg 
 |-  ( ( X e. A /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
28 5 8 27 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
29 26 28 eqtrd 
 |-  ( ph -> ( X ( 1st ` ( C 1stF D ) ) Y ) = X )
30 14 20 29 3eqtrd 
 |-  ( ph -> ( ( 1st ` K ) ` Y ) = X )