Metamath Proof Explorer

Theorem yonedalem1

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses yoneda.y 
|- Y = ( Yon ` C )
yoneda.b 
|- B = ( Base ` C )
yoneda.1 
|- .1. = ( Id ` C )
yoneda.o 
|- O = ( oppCat ` C )
yoneda.s 
|- S = ( SetCat ` U )
yoneda.t 
|- T = ( SetCat ` V )
yoneda.q 
|- Q = ( O FuncCat S )
yoneda.h 
|- H = ( HomF ` Q )
yoneda.r 
|- R = ( ( Q Xc. O ) FuncCat T )
yoneda.e 
|- E = ( O evalF S )
yoneda.z 
|- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
yoneda.c 
|- ( ph -> C e. Cat )
yoneda.w 
|- ( ph -> V e. W )
yoneda.u 
|- ( ph -> ran ( Homf ` C ) C_ U )
yoneda.v 
|- ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
Assertion yonedalem1 
|- ( ph -> ( Z e. ( ( Q Xc. O ) Func T ) /\ E e. ( ( Q Xc. O ) Func T ) ) )

Proof

Step Hyp Ref Expression
1 yoneda.y 
 |-  Y = ( Yon ` C )
2 yoneda.b 
 |-  B = ( Base ` C )
3 yoneda.1 
 |-  .1. = ( Id ` C )
4 yoneda.o 
 |-  O = ( oppCat ` C )
5 yoneda.s 
 |-  S = ( SetCat ` U )
6 yoneda.t 
 |-  T = ( SetCat ` V )
7 yoneda.q 
 |-  Q = ( O FuncCat S )
8 yoneda.h 
 |-  H = ( HomF ` Q )
9 yoneda.r 
 |-  R = ( ( Q Xc. O ) FuncCat T )
10 yoneda.e 
 |-  E = ( O evalF S )
11 yoneda.z 
 |-  Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
12 yoneda.c 
 |-  ( ph -> C e. Cat )
13 yoneda.w 
 |-  ( ph -> V e. W )
14 yoneda.u 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
15 yoneda.v 
 |-  ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
16 eqid 
 |-  ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) = ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) )
17 eqid 
 |-  ( ( oppCat ` Q ) Xc. Q ) = ( ( oppCat ` Q ) Xc. Q )
18 eqid 
 |-  ( Q Xc. O ) = ( Q Xc. O )
19 4 oppccat 
 |-  ( C e. Cat -> O e. Cat )
20 12 19 syl 
 |-  ( ph -> O e. Cat )
21 15 unssbd 
 |-  ( ph -> U C_ V )
22 13 21 ssexd 
 |-  ( ph -> U e. _V )
23 5 setccat 
 |-  ( U e. _V -> S e. Cat )
24 22 23 syl 
 |-  ( ph -> S e. Cat )
25 7 20 24 fuccat 
 |-  ( ph -> Q e. Cat )
26 eqid 
 |-  ( Q 2ndF O ) = ( Q 2ndF O )
27 18 25 20 26 2ndfcl 
 |-  ( ph -> ( Q 2ndF O ) e. ( ( Q Xc. O ) Func O ) )
28 eqid 
 |-  ( oppCat ` Q ) = ( oppCat ` Q )
29 relfunc 
 |-  Rel ( C Func Q )
30 1 12 4 5 7 22 14 yoncl 
 |-  ( ph -> Y e. ( C Func Q ) )
31 1st2ndbr 
 |-  ( ( Rel ( C Func Q ) /\ Y e. ( C Func Q ) ) -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
32 29 30 31 sylancr 
 |-  ( ph -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
33 4 28 32 funcoppc 
 |-  ( ph -> ( 1st ` Y ) ( O Func ( oppCat ` Q ) ) tpos ( 2nd ` Y ) )
34 df-br 
 |-  ( ( 1st ` Y ) ( O Func ( oppCat ` Q ) ) tpos ( 2nd ` Y ) <-> <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. e. ( O Func ( oppCat ` Q ) ) )
35 33 34 sylib 
 |-  ( ph -> <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. e. ( O Func ( oppCat ` Q ) ) )
36 27 35 cofucl 
 |-  ( ph -> ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) e. ( ( Q Xc. O ) Func ( oppCat ` Q ) ) )
37 eqid 
 |-  ( Q 1stF O ) = ( Q 1stF O )
38 18 25 20 37 1stfcl 
 |-  ( ph -> ( Q 1stF O ) e. ( ( Q Xc. O ) Func Q ) )
39 16 17 36 38 prfcl 
 |-  ( ph -> ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) e. ( ( Q Xc. O ) Func ( ( oppCat ` Q ) Xc. Q ) ) )
40 15 unssad 
 |-  ( ph -> ran ( Homf ` Q ) C_ V )
41 8 28 6 25 13 40 hofcl 
 |-  ( ph -> H e. ( ( ( oppCat ` Q ) Xc. Q ) Func T ) )
42 39 41 cofucl 
 |-  ( ph -> ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) e. ( ( Q Xc. O ) Func T ) )
43 11 42 eqeltrid 
 |-  ( ph -> Z e. ( ( Q Xc. O ) Func T ) )
44 6 5 13 21 funcsetcres2 
 |-  ( ph -> ( ( Q Xc. O ) Func S ) C_ ( ( Q Xc. O ) Func T ) )
45 10 7 20 24 evlfcl 
 |-  ( ph -> E e. ( ( Q Xc. O ) Func S ) )
46 44 45 sseldd 
 |-  ( ph -> E e. ( ( Q Xc. O ) Func T ) )
47 43 46 jca 
 |-  ( ph -> ( Z e. ( ( Q Xc. O ) Func T ) /\ E e. ( ( Q Xc. O ) Func T ) ) )