Metamath Proof Explorer


Theorem oyoncl

Description: The opposite Yoneda embedding is a functor from oppCatC to the functor category C -> SetCat . (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses oyoncl.o
|- O = ( oppCat ` C )
oyoncl.y
|- Y = ( Yon ` O )
oyoncl.c
|- ( ph -> C e. Cat )
oyoncl.s
|- S = ( SetCat ` U )
oyoncl.u
|- ( ph -> U e. V )
oyoncl.h
|- ( ph -> ran ( Homf ` C ) C_ U )
oyoncl.q
|- Q = ( C FuncCat S )
Assertion oyoncl
|- ( ph -> Y e. ( O Func Q ) )

Proof

Step Hyp Ref Expression
1 oyoncl.o
 |-  O = ( oppCat ` C )
2 oyoncl.y
 |-  Y = ( Yon ` O )
3 oyoncl.c
 |-  ( ph -> C e. Cat )
4 oyoncl.s
 |-  S = ( SetCat ` U )
5 oyoncl.u
 |-  ( ph -> U e. V )
6 oyoncl.h
 |-  ( ph -> ran ( Homf ` C ) C_ U )
7 oyoncl.q
 |-  Q = ( C FuncCat S )
8 1 oppccat
 |-  ( C e. Cat -> O e. Cat )
9 3 8 syl
 |-  ( ph -> O e. Cat )
10 eqid
 |-  ( oppCat ` O ) = ( oppCat ` O )
11 eqid
 |-  ( ( oppCat ` O ) FuncCat S ) = ( ( oppCat ` O ) FuncCat S )
12 eqid
 |-  ( Homf ` C ) = ( Homf ` C )
13 1 12 oppchomf
 |-  tpos ( Homf ` C ) = ( Homf ` O )
14 13 rneqi
 |-  ran tpos ( Homf ` C ) = ran ( Homf ` O )
15 relxp
 |-  Rel ( ( Base ` C ) X. ( Base ` C ) )
16 eqid
 |-  ( Base ` C ) = ( Base ` C )
17 12 16 homffn
 |-  ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) )
18 17 fndmi
 |-  dom ( Homf ` C ) = ( ( Base ` C ) X. ( Base ` C ) )
19 18 releqi
 |-  ( Rel dom ( Homf ` C ) <-> Rel ( ( Base ` C ) X. ( Base ` C ) ) )
20 15 19 mpbir
 |-  Rel dom ( Homf ` C )
21 rntpos
 |-  ( Rel dom ( Homf ` C ) -> ran tpos ( Homf ` C ) = ran ( Homf ` C ) )
22 20 21 ax-mp
 |-  ran tpos ( Homf ` C ) = ran ( Homf ` C )
23 14 22 eqtr3i
 |-  ran ( Homf ` O ) = ran ( Homf ` C )
24 23 6 eqsstrid
 |-  ( ph -> ran ( Homf ` O ) C_ U )
25 2 9 10 4 11 5 24 yoncl
 |-  ( ph -> Y e. ( O Func ( ( oppCat ` O ) FuncCat S ) ) )
26 1 2oppchomf
 |-  ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
27 26 a1i
 |-  ( ph -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
28 1 2oppccomf
 |-  ( comf ` C ) = ( comf ` ( oppCat ` O ) )
29 28 a1i
 |-  ( ph -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
30 eqidd
 |-  ( ph -> ( Homf ` S ) = ( Homf ` S ) )
31 eqidd
 |-  ( ph -> ( comf ` S ) = ( comf ` S ) )
32 10 oppccat
 |-  ( O e. Cat -> ( oppCat ` O ) e. Cat )
33 9 32 syl
 |-  ( ph -> ( oppCat ` O ) e. Cat )
34 4 setccat
 |-  ( U e. V -> S e. Cat )
35 5 34 syl
 |-  ( ph -> S e. Cat )
36 27 29 30 31 3 33 35 35 fucpropd
 |-  ( ph -> ( C FuncCat S ) = ( ( oppCat ` O ) FuncCat S ) )
37 7 36 eqtrid
 |-  ( ph -> Q = ( ( oppCat ` O ) FuncCat S ) )
38 37 oveq2d
 |-  ( ph -> ( O Func Q ) = ( O Func ( ( oppCat ` O ) FuncCat S ) ) )
39 25 38 eleqtrrd
 |-  ( ph -> Y e. ( O Func Q ) )