Metamath Proof Explorer

Theorem yon12

Description: Value of the Yoneda embedding at a morphism. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (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 )
yon12.f 
|- ( ph -> F e. ( W H Z ) )
yon12.g 
|- ( ph -> G e. ( Z H X ) )
Assertion yon12 
|- ( ph -> ( ( ( Z ( 2nd ` ( ( 1st ` Y ) ` X ) ) W ) ` F ) ` G ) = ( G ( <. W , Z >. .x. X ) F ) )

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 yon12.f 
 |-  ( ph -> F e. ( W H Z ) )
10 yon12.g 
 |-  ( ph -> G e. ( Z 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 -> ( 1st ` Y ) = ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) )
15 14 fveq1d 
 |-  ( ph -> ( ( 1st ` Y ) ` X ) = ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) )
16 15 fveq2d 
 |-  ( ph -> ( 2nd ` ( ( 1st ` Y ) ` X ) ) = ( 2nd ` ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) ) )
17 16 oveqd 
 |-  ( ph -> ( Z ( 2nd ` ( ( 1st ` Y ) ` X ) ) W ) = ( Z ( 2nd ` ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) ) W ) )
18 17 fveq1d 
 |-  ( ph -> ( ( Z ( 2nd ` ( ( 1st ` Y ) ` X ) ) W ) ` F ) = ( ( Z ( 2nd ` ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) ) W ) ` F ) )
19 eqid 
 |-  ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) = ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) )
20 11 oppccat 
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
21 3 20 syl 
 |-  ( ph -> ( oppCat ` C ) e. Cat )
22 eqid 
 |-  ( SetCat ` ran ( Homf ` C ) ) = ( SetCat ` ran ( Homf ` C ) )
23 fvex 
 |-  ( Homf ` C ) e. _V
24 23 rnex 
 |-  ran ( Homf ` C ) e. _V
25 24 a1i 
 |-  ( ph -> ran ( Homf ` C ) e. _V )
26 ssidd 
 |-  ( ph -> ran ( Homf ` C ) C_ ran ( Homf ` C ) )
27 11 12 22 3 25 26 oppchofcl 
 |-  ( ph -> ( HomF ` ( oppCat ` C ) ) e. ( ( C Xc. ( oppCat ` C ) ) Func ( SetCat ` ran ( Homf ` C ) ) ) )
28 11 2 oppcbas 
 |-  B = ( Base ` ( oppCat ` C ) )
29 eqid 
 |-  ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) = ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X )
30 eqid 
 |-  ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) )
31 eqid 
 |-  ( Id ` C ) = ( Id ` C )
32 5 11 oppchom 
 |-  ( Z ( Hom ` ( oppCat ` C ) ) W ) = ( W H Z )
33 9 32 eleqtrrdi 
 |-  ( ph -> F e. ( Z ( Hom ` ( oppCat ` C ) ) W ) )
34 19 2 3 21 27 28 4 29 6 30 31 8 33 curf12 
 |-  ( ph -> ( ( Z ( 2nd ` ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) ) W ) ` F ) = ( ( ( Id ` C ) ` X ) ( <. X , Z >. ( 2nd ` ( HomF ` ( oppCat ` C ) ) ) <. X , W >. ) F ) )
35 18 34 eqtrd 
 |-  ( ph -> ( ( Z ( 2nd ` ( ( 1st ` Y ) ` X ) ) W ) ` F ) = ( ( ( Id ` C ) ` X ) ( <. X , Z >. ( 2nd ` ( HomF ` ( oppCat ` C ) ) ) <. X , W >. ) F ) )
36 35 fveq1d 
 |-  ( ph -> ( ( ( Z ( 2nd ` ( ( 1st ` Y ) ` X ) ) W ) ` F ) ` G ) = ( ( ( ( Id ` C ) ` X ) ( <. X , Z >. ( 2nd ` ( HomF ` ( oppCat ` C ) ) ) <. X , W >. ) F ) ` G ) )
37 eqid 
 |-  ( comp ` ( oppCat ` C ) ) = ( comp ` ( oppCat ` C ) )
38 2 5 31 3 4 catidcl 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X H X ) )
39 5 11 oppchom 
 |-  ( X ( Hom ` ( oppCat ` C ) ) X ) = ( X H X )
40 38 39 eleqtrrdi 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X ( Hom ` ( oppCat ` C ) ) X ) )
41 5 11 oppchom 
 |-  ( X ( Hom ` ( oppCat ` C ) ) Z ) = ( Z H X )
42 10 41 eleqtrrdi 
 |-  ( ph -> G e. ( X ( Hom ` ( oppCat ` C ) ) Z ) )
43 12 21 28 30 4 6 4 8 37 40 33 42 hof2 
 |-  ( ph -> ( ( ( ( Id ` C ) ` X ) ( <. X , Z >. ( 2nd ` ( HomF ` ( oppCat ` C ) ) ) <. X , W >. ) F ) ` G ) = ( ( F ( <. X , Z >. ( comp ` ( oppCat ` C ) ) W ) G ) ( <. X , X >. ( comp ` ( oppCat ` C ) ) W ) ( ( Id ` C ) ` X ) ) )
44 2 7 11 4 6 8 oppcco 
 |-  ( ph -> ( F ( <. X , Z >. ( comp ` ( oppCat ` C ) ) W ) G ) = ( G ( <. W , Z >. .x. X ) F ) )
45 44 oveq1d 
 |-  ( ph -> ( ( F ( <. X , Z >. ( comp ` ( oppCat ` C ) ) W ) G ) ( <. X , X >. ( comp ` ( oppCat ` C ) ) W ) ( ( Id ` C ) ` X ) ) = ( ( G ( <. W , Z >. .x. X ) F ) ( <. X , X >. ( comp ` ( oppCat ` C ) ) W ) ( ( Id ` C ) ` X ) ) )
46 2 7 11 4 4 8 oppcco 
 |-  ( ph -> ( ( G ( <. W , Z >. .x. X ) F ) ( <. X , X >. ( comp ` ( oppCat ` C ) ) W ) ( ( Id ` C ) ` X ) ) = ( ( ( Id ` C ) ` X ) ( <. W , X >. .x. X ) ( G ( <. W , Z >. .x. X ) F ) ) )
47 2 5 7 3 8 6 4 9 10 catcocl 
 |-  ( ph -> ( G ( <. W , Z >. .x. X ) F ) e. ( W H X ) )
48 2 5 31 3 8 7 4 47 catlid 
 |-  ( ph -> ( ( ( Id ` C ) ` X ) ( <. W , X >. .x. X ) ( G ( <. W , Z >. .x. X ) F ) ) = ( G ( <. W , Z >. .x. X ) F ) )
49 45 46 48 3eqtrd 
 |-  ( ph -> ( ( F ( <. X , Z >. ( comp ` ( oppCat ` C ) ) W ) G ) ( <. X , X >. ( comp ` ( oppCat ` C ) ) W ) ( ( Id ` C ) ` X ) ) = ( G ( <. W , Z >. .x. X ) F ) )
50 36 43 49 3eqtrd 
 |-  ( ph -> ( ( ( Z ( 2nd ` ( ( 1st ` Y ) ` X ) ) W ) ` F ) ` G ) = ( G ( <. W , Z >. .x. X ) F ) )