Metamath Proof Explorer

Theorem yonffth

Description: The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category C as a full subcategory of the category Q of presheaves on C . (Contributed by Mario Carneiro, 29-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 yonffth.y 
 |-  Y = ( Yon ` C )
2 yonffth.o 
 |-  O = ( oppCat ` C )
3 yonffth.s 
 |-  S = ( SetCat ` U )
4 yonffth.q 
 |-  Q = ( O FuncCat S )
5 yonffth.c 
 |-  ( ph -> C e. Cat )
6 yonffth.u 
 |-  ( ph -> U e. V )
7 yonffth.h 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( Id ` C ) = ( Id ` C )
10 eqid 
 |-  ( SetCat ` ( ran ( Homf ` Q ) u. U ) ) = ( SetCat ` ( ran ( Homf ` Q ) u. U ) )
11 eqid 
 |-  ( HomF ` Q ) = ( HomF ` Q )
12 eqid 
 |-  ( ( Q Xc. O ) FuncCat ( SetCat ` ( ran ( Homf ` Q ) u. U ) ) ) = ( ( Q Xc. O ) FuncCat ( SetCat ` ( ran ( Homf ` Q ) u. U ) ) )
13 eqid 
 |-  ( O evalF S ) = ( O evalF S )
14 eqid 
 |-  ( ( HomF ` Q ) o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) = ( ( HomF ` Q ) o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
15 fvex 
 |-  ( Homf ` Q ) e. _V
16 15 rnex 
 |-  ran ( Homf ` Q ) e. _V
17 unexg 
 |-  ( ( ran ( Homf ` Q ) e. _V /\ U e. V ) -> ( ran ( Homf ` Q ) u. U ) e. _V )
18 16 6 17 sylancr 
 |-  ( ph -> ( ran ( Homf ` Q ) u. U ) e. _V )
19 ssidd 
 |-  ( ph -> ( ran ( Homf ` Q ) u. U ) C_ ( ran ( Homf ` Q ) u. U ) )
20 eqid 
 |-  ( f e. ( O Func S ) , x e. ( Base ` C ) |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( ( Id ` C ) ` x ) ) ) ) = ( f e. ( O Func S ) , x e. ( Base ` C ) |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( ( Id ` C ) ` x ) ) ) )
21 eqid 
 |-  ( Inv ` ( ( Q Xc. O ) FuncCat ( SetCat ` ( ran ( Homf ` Q ) u. U ) ) ) ) = ( Inv ` ( ( Q Xc. O ) FuncCat ( SetCat ` ( ran ( Homf ` Q ) u. U ) ) ) )
22 eqid 
 |-  ( f e. ( O Func S ) , x e. ( Base ` C ) |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. ( Base ` C ) |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) ) = ( f e. ( O Func S ) , x e. ( Base ` C ) |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. ( Base ` C ) |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )
23 1 8 9 2 3 10 4 11 12 13 14 5 18 7 19 20 21 22 yonffthlem 
 |-  ( ph -> Y e. ( ( C Full Q ) i^i ( C Faith Q ) ) )