Metamath Proof Explorer

Theorem yon11

Description: Value of the Yoneda embedding at an object. 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 )
Assertion yon11 
|- ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` Z ) = ( Z H X ) )

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 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
8 eqid 
 |-  ( HomF ` ( oppCat ` C ) ) = ( HomF ` ( oppCat ` C ) )
9 1 3 7 8 yonval 
 |-  ( ph -> Y = ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) )
10 9 fveq2d 
 |-  ( ph -> ( 1st ` Y ) = ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) )
11 10 fveq1d 
 |-  ( ph -> ( ( 1st ` Y ) ` X ) = ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) )
12 11 fveq2d 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) = ( 1st ` ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) ) )
13 12 fveq1d 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` Z ) = ( ( 1st ` ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) ) ` Z ) )
14 eqid 
 |-  ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) = ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) )
15 7 oppccat 
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
16 3 15 syl 
 |-  ( ph -> ( oppCat ` C ) e. Cat )
17 eqid 
 |-  ( SetCat ` ran ( Homf ` C ) ) = ( SetCat ` ran ( Homf ` C ) )
18 fvex 
 |-  ( Homf ` C ) e. _V
19 18 rnex 
 |-  ran ( Homf ` C ) e. _V
20 19 a1i 
 |-  ( ph -> ran ( Homf ` C ) e. _V )
21 ssidd 
 |-  ( ph -> ran ( Homf ` C ) C_ ran ( Homf ` C ) )
22 7 8 17 3 20 21 oppchofcl 
 |-  ( ph -> ( HomF ` ( oppCat ` C ) ) e. ( ( C Xc. ( oppCat ` C ) ) Func ( SetCat ` ran ( Homf ` C ) ) ) )
23 7 2 oppcbas 
 |-  B = ( Base ` ( oppCat ` C ) )
24 eqid 
 |-  ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) = ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X )
25 14 2 3 16 22 23 4 24 6 curf11 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) ) ` X ) ) ` Z ) = ( X ( 1st ` ( HomF ` ( oppCat ` C ) ) ) Z ) )
26 eqid 
 |-  ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) )
27 8 16 23 26 4 6 hof1 
 |-  ( ph -> ( X ( 1st ` ( HomF ` ( oppCat ` C ) ) ) Z ) = ( X ( Hom ` ( oppCat ` C ) ) Z ) )
28 5 7 oppchom 
 |-  ( X ( Hom ` ( oppCat ` C ) ) Z ) = ( Z H X )
29 27 28 eqtrdi 
 |-  ( ph -> ( X ( 1st ` ( HomF ` ( oppCat ` C ) ) ) Z ) = ( Z H X ) )
30 13 25 29 3eqtrd 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` Z ) = ( Z H X ) )