MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  yonval Structured version   Unicode version

Theorem yonval 15854
Description: Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.)
Hypotheses
Ref Expression
yonval.y  |-  Y  =  (Yon `  C )
yonval.c  |-  ( ph  ->  C  e.  Cat )
yonval.o  |-  O  =  (oppCat `  C )
yonval.m  |-  M  =  (HomF
`  O )
Assertion
Ref Expression
yonval  |-  ( ph  ->  Y  =  ( <. C ,  O >. curryF  M ) )

Proof of Theorem yonval
Dummy variable  c is distinct from all other variables.
StepHypRef Expression
1 yonval.y . 2  |-  Y  =  (Yon `  C )
2 df-yon 15844 . . . 4  |- Yon  =  ( c  e.  Cat  |->  (
<. c ,  (oppCat `  c ) >. curryF  (HomF
`  (oppCat `  c )
) ) )
32a1i 11 . . 3  |-  ( ph  -> Yon  =  ( c  e. 
Cat  |->  ( <. c ,  (oppCat `  c ) >. curryF  (HomF `  (oppCat `  c ) ) ) ) )
4 simpr 459 . . . . 5  |-  ( (
ph  /\  c  =  C )  ->  c  =  C )
54fveq2d 5853 . . . . . 6  |-  ( (
ph  /\  c  =  C )  ->  (oppCat `  c )  =  (oppCat `  C ) )
6 yonval.o . . . . . 6  |-  O  =  (oppCat `  C )
75, 6syl6eqr 2461 . . . . 5  |-  ( (
ph  /\  c  =  C )  ->  (oppCat `  c )  =  O )
84, 7opeq12d 4167 . . . 4  |-  ( (
ph  /\  c  =  C )  ->  <. c ,  (oppCat `  c ) >.  =  <. C ,  O >. )
97fveq2d 5853 . . . . 5  |-  ( (
ph  /\  c  =  C )  ->  (HomF `  (oppCat `  c ) )  =  (HomF
`  O ) )
10 yonval.m . . . . 5  |-  M  =  (HomF
`  O )
119, 10syl6eqr 2461 . . . 4  |-  ( (
ph  /\  c  =  C )  ->  (HomF `  (oppCat `  c ) )  =  M )
128, 11oveq12d 6296 . . 3  |-  ( (
ph  /\  c  =  C )  ->  ( <. c ,  (oppCat `  c ) >. curryF  (HomF
`  (oppCat `  c )
) )  =  (
<. C ,  O >. curryF  M ) )
13 yonval.c . . 3  |-  ( ph  ->  C  e.  Cat )
14 ovex 6306 . . . 4  |-  ( <. C ,  O >. curryF  M )  e.  _V
1514a1i 11 . . 3  |-  ( ph  ->  ( <. C ,  O >. curryF  M
)  e.  _V )
163, 12, 13, 15fvmptd 5938 . 2  |-  ( ph  ->  (Yon `  C )  =  ( <. C ,  O >. curryF  M ) )
171, 16syl5eq 2455 1  |-  ( ph  ->  Y  =  ( <. C ,  O >. curryF  M ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842   _Vcvv 3059   <.cop 3978    |-> cmpt 4453   ` cfv 5569  (class class class)co 6278   Catccat 15278  oppCatcoppc 15324   curryF ccurf 15803  HomFchof 15841  Yoncyon 15842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-iota 5533  df-fun 5571  df-fv 5577  df-ov 6281  df-yon 15844
This theorem is referenced by:  yoncl  15855  yon11  15857  yon12  15858  yon2  15859  yonpropd  15861  oppcyon  15862
  Copyright terms: Public domain W3C validator