Metamath Proof Explorer

Theorem yonval

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

Ref Expression
Hypotheses yonval.y 
|- Y = ( Yon ` C )
yonval.c 
|- ( ph -> C e. Cat )
yonval.o 
|- O = ( oppCat ` C )
yonval.m 
|- M = ( HomF ` O )
Assertion yonval 
|- ( ph -> Y = ( <. C , O >. curryF M ) )

Proof

Step Hyp Ref Expression
1 yonval.y 
 |-  Y = ( Yon ` C )
2 yonval.c 
 |-  ( ph -> C e. Cat )
3 yonval.o 
 |-  O = ( oppCat ` C )
4 yonval.m 
 |-  M = ( HomF ` O )
5 df-yon 
 |-  Yon = ( c e. Cat |-> ( <. c , ( oppCat ` c ) >. curryF ( HomF ` ( oppCat ` c ) ) ) )
6 simpr 
 |-  ( ( ph /\ c = C ) -> c = C )
7 6 fveq2d 
 |-  ( ( ph /\ c = C ) -> ( oppCat ` c ) = ( oppCat ` C ) )
8 7 3 eqtr4di 
 |-  ( ( ph /\ c = C ) -> ( oppCat ` c ) = O )
9 6 8 opeq12d 
 |-  ( ( ph /\ c = C ) -> <. c , ( oppCat ` c ) >. = <. C , O >. )
10 8 fveq2d 
 |-  ( ( ph /\ c = C ) -> ( HomF ` ( oppCat ` c ) ) = ( HomF ` O ) )
11 10 4 eqtr4di 
 |-  ( ( ph /\ c = C ) -> ( HomF ` ( oppCat ` c ) ) = M )
12 9 11 oveq12d 
 |-  ( ( ph /\ c = C ) -> ( <. c , ( oppCat ` c ) >. curryF ( HomF ` ( oppCat ` c ) ) ) = ( <. C , O >. curryF M ) )
13 ovexd 
 |-  ( ph -> ( <. C , O >. curryF M ) e. _V )
14 5 12 2 13 fvmptd2 
 |-  ( ph -> ( Yon ` C ) = ( <. C , O >. curryF M ) )
15 1 14 syl5eq 
 |-  ( ph -> Y = ( <. C , O >. curryF M ) )