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 eqtrid
 |-  ( ph -> Y = ( <. C , O >. curryF M ) )