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 syl5eq 
 |-  ( 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 ) )