Metamath Proof Explorer

Theorem yon2

Description: Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses yon11.y 
|- Y = ( Yon ` C )
yon11.b 
|- B = ( Base ` C )
yon11.c 
|- ( ph -> C e. Cat )
yon11.p 
|- ( ph -> X e. B )
yon11.h 
|- H = ( Hom ` C )
yon11.z 
|- ( ph -> Z e. B )
yon12.x 
|- .x. = ( comp ` C )
yon12.w 
|- ( ph -> W e. B )
yon2.f 
|- ( ph -> F e. ( X H Z ) )
yon2.g 
|- ( ph -> G e. ( W H X ) )
Assertion yon2 
|- ( ph -> ( ( ( ( X ( 2nd ` Y ) Z ) ` F ) ` W ) ` G ) = ( F ( <. W , X >. .x. Z ) G ) )

Proof

Step Hyp Ref Expression
1 yon11.y 
 |-  Y = ( Yon ` C )
2 yon11.b 
 |-  B = ( Base ` C )
3 yon11.c 
 |-  ( ph -> C e. Cat )
4 yon11.p 
 |-  ( ph -> X e. B )
5 yon11.h 
 |-  H = ( Hom ` C )
6 yon11.z 
 |-  ( ph -> Z e. B )
7 yon12.x 
 |-  .x. = ( comp ` C )
8 yon12.w 
 |-  ( ph -> W e. B )
9 yon2.f 
 |-  ( ph -> F e. ( X H Z ) )
10 yon2.g 
 |-  ( ph -> G e. ( W H X ) )
11 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
12 eqid 
 |-  ( HomF ` ( oppCat ` C ) ) = ( HomF ` ( oppCat ` C ) )
13 1 3 11 12 yonval 
 |-  ( ph -> Y = ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) )
14 13 fveq2d 
 |-  ( ph -> ( 2nd ` Y ) = ( 2nd ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) )
15 14 oveqd 
 |-  ( ph -> ( X ( 2nd ` Y ) Z ) = ( X ( 2nd ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) Z ) )
16 15 fveq1d 
 |-  ( ph -> ( ( X ( 2nd ` Y ) Z ) ` F ) = ( ( X ( 2nd ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) Z ) ` F ) )
17 16 fveq1d 
 |-  ( ph -> ( ( ( X ( 2nd ` Y ) Z ) ` F ) ` W ) = ( ( ( X ( 2nd ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) Z ) ` F ) ` W ) )
18 eqid 
 |-  ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) = ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) )
19 11 oppccat 
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
20 3 19 syl 
 |-  ( ph -> ( oppCat ` C ) e. Cat )
21 eqid 
 |-  ( SetCat ` ran ( Homf ` C ) ) = ( SetCat ` ran ( Homf ` C ) )
22 fvex 
 |-  ( Homf ` C ) e. _V
23 22 rnex 
 |-  ran ( Homf ` C ) e. _V
24 23 a1i 
 |-  ( ph -> ran ( Homf ` C ) e. _V )
25 ssidd 
 |-  ( ph -> ran ( Homf ` C ) C_ ran ( Homf ` C ) )
26 11 12 21 3 24 25 oppchofcl 
 |-  ( ph -> ( HomF ` ( oppCat ` C ) ) e. ( ( C Xc. ( oppCat ` C ) ) Func ( SetCat ` ran ( Homf ` C ) ) ) )
27 11 2 oppcbas 
 |-  B = ( Base ` ( oppCat ` C ) )
28 eqid 
 |-  ( Id ` ( oppCat ` C ) ) = ( Id ` ( oppCat ` C ) )
29 eqid 
 |-  ( ( X ( 2nd ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) Z ) ` F ) = ( ( X ( 2nd ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) Z ) ` F )
30 18 2 3 20 26 27 5 28 4 6 9 29 8 curf2val 
 |-  ( ph -> ( ( ( X ( 2nd ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) Z ) ` F ) ` W ) = ( F ( <. X , W >. ( 2nd ` ( HomF ` ( oppCat ` C ) ) ) <. Z , W >. ) ( ( Id ` ( oppCat ` C ) ) ` W ) ) )
31 17 30 eqtrd 
 |-  ( ph -> ( ( ( X ( 2nd ` Y ) Z ) ` F ) ` W ) = ( F ( <. X , W >. ( 2nd ` ( HomF ` ( oppCat ` C ) ) ) <. Z , W >. ) ( ( Id ` ( oppCat ` C ) ) ` W ) ) )
32 31 fveq1d 
 |-  ( ph -> ( ( ( ( X ( 2nd ` Y ) Z ) ` F ) ` W ) ` G ) = ( ( F ( <. X , W >. ( 2nd ` ( HomF ` ( oppCat ` C ) ) ) <. Z , W >. ) ( ( Id ` ( oppCat ` C ) ) ` W ) ) ` G ) )
33 eqid 
 |-  ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) )
34 eqid 
 |-  ( comp ` ( oppCat ` C ) ) = ( comp ` ( oppCat ` C ) )
35 5 11 oppchom 
 |-  ( Z ( Hom ` ( oppCat ` C ) ) X ) = ( X H Z )
36 9 35 eleqtrrdi 
 |-  ( ph -> F e. ( Z ( Hom ` ( oppCat ` C ) ) X ) )
37 27 33 28 20 8 catidcl 
 |-  ( ph -> ( ( Id ` ( oppCat ` C ) ) ` W ) e. ( W ( Hom ` ( oppCat ` C ) ) W ) )
38 5 11 oppchom 
 |-  ( X ( Hom ` ( oppCat ` C ) ) W ) = ( W H X )
39 10 38 eleqtrrdi 
 |-  ( ph -> G e. ( X ( Hom ` ( oppCat ` C ) ) W ) )
40 12 20 27 33 4 8 6 8 34 36 37 39 hof2 
 |-  ( ph -> ( ( F ( <. X , W >. ( 2nd ` ( HomF ` ( oppCat ` C ) ) ) <. Z , W >. ) ( ( Id ` ( oppCat ` C ) ) ` W ) ) ` G ) = ( ( ( ( Id ` ( oppCat ` C ) ) ` W ) ( <. X , W >. ( comp ` ( oppCat ` C ) ) W ) G ) ( <. Z , X >. ( comp ` ( oppCat ` C ) ) W ) F ) )
41 27 33 28 20 4 34 8 39 catlid 
 |-  ( ph -> ( ( ( Id ` ( oppCat ` C ) ) ` W ) ( <. X , W >. ( comp ` ( oppCat ` C ) ) W ) G ) = G )
42 41 oveq1d 
 |-  ( ph -> ( ( ( ( Id ` ( oppCat ` C ) ) ` W ) ( <. X , W >. ( comp ` ( oppCat ` C ) ) W ) G ) ( <. Z , X >. ( comp ` ( oppCat ` C ) ) W ) F ) = ( G ( <. Z , X >. ( comp ` ( oppCat ` C ) ) W ) F ) )
43 2 7 11 6 4 8 oppcco 
 |-  ( ph -> ( G ( <. Z , X >. ( comp ` ( oppCat ` C ) ) W ) F ) = ( F ( <. W , X >. .x. Z ) G ) )
44 42 43 eqtrd 
 |-  ( ph -> ( ( ( ( Id ` ( oppCat ` C ) ) ` W ) ( <. X , W >. ( comp ` ( oppCat ` C ) ) W ) G ) ( <. Z , X >. ( comp ` ( oppCat ` C ) ) W ) F ) = ( F ( <. W , X >. .x. Z ) G ) )
45 32 40 44 3eqtrd 
 |-  ( ph -> ( ( ( ( X ( 2nd ` Y ) Z ) ` F ) ` W ) ` G ) = ( F ( <. W , X >. .x. Z ) G ) )