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 eqtrid
 |-  ( 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 eqtrid
 |-  ( 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 )