Metamath Proof Explorer

Theorem yonedalem21

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 )
yonedalem21.f 
|- ( ph -> F e. ( O Func S ) )
yonedalem21.x 
|- ( ph -> X e. B )
Assertion yonedalem21 
|- ( ph -> ( F ( 1st ` Z ) X ) = ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )

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 yonedalem21.f 
 |-  ( ph -> F e. ( O Func S ) )
17 yonedalem21.x 
 |-  ( ph -> X e. B )
18 11 fveq2i 
 |-  ( 1st ` Z ) = ( 1st ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) )
19 18 oveqi 
 |-  ( F ( 1st ` Z ) X ) = ( F ( 1st ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) X )
20 df-ov 
 |-  ( F ( 1st ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) X ) = ( ( 1st ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) ` <. F , X >. )
21 19 20 eqtri 
 |-  ( F ( 1st ` Z ) X ) = ( ( 1st ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) ` <. F , X >. )
22 eqid 
 |-  ( Q Xc. O ) = ( Q Xc. O )
23 7 fucbas 
 |-  ( O Func S ) = ( Base ` Q )
24 4 2 oppcbas 
 |-  B = ( Base ` O )
25 22 23 24 xpcbas 
 |-  ( ( O Func S ) X. B ) = ( Base ` ( Q Xc. O ) )
26 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 ) )
27 eqid 
 |-  ( ( oppCat ` Q ) Xc. Q ) = ( ( oppCat ` Q ) Xc. Q )
28 4 oppccat 
 |-  ( C e. Cat -> O e. Cat )
29 12 28 syl 
 |-  ( ph -> O e. Cat )
30 15 unssbd 
 |-  ( ph -> U C_ V )
31 13 30 ssexd 
 |-  ( ph -> U e. _V )
32 5 setccat 
 |-  ( U e. _V -> S e. Cat )
33 31 32 syl 
 |-  ( ph -> S e. Cat )
34 7 29 33 fuccat 
 |-  ( ph -> Q e. Cat )
35 eqid 
 |-  ( Q 2ndF O ) = ( Q 2ndF O )
36 22 34 29 35 2ndfcl 
 |-  ( ph -> ( Q 2ndF O ) e. ( ( Q Xc. O ) Func O ) )
37 eqid 
 |-  ( oppCat ` Q ) = ( oppCat ` Q )
38 relfunc 
 |-  Rel ( C Func Q )
39 1 12 4 5 7 31 14 yoncl 
 |-  ( ph -> Y e. ( C Func Q ) )
40 1st2ndbr 
 |-  ( ( Rel ( C Func Q ) /\ Y e. ( C Func Q ) ) -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
41 38 39 40 sylancr 
 |-  ( ph -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
42 4 37 41 funcoppc 
 |-  ( ph -> ( 1st ` Y ) ( O Func ( oppCat ` Q ) ) tpos ( 2nd ` Y ) )
43 df-br 
 |-  ( ( 1st ` Y ) ( O Func ( oppCat ` Q ) ) tpos ( 2nd ` Y ) <-> <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. e. ( O Func ( oppCat ` Q ) ) )
44 42 43 sylib 
 |-  ( ph -> <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. e. ( O Func ( oppCat ` Q ) ) )
45 36 44 cofucl 
 |-  ( ph -> ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) e. ( ( Q Xc. O ) Func ( oppCat ` Q ) ) )
46 eqid 
 |-  ( Q 1stF O ) = ( Q 1stF O )
47 22 34 29 46 1stfcl 
 |-  ( ph -> ( Q 1stF O ) e. ( ( Q Xc. O ) Func Q ) )
48 26 27 45 47 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 ) ) )
49 15 unssad 
 |-  ( ph -> ran ( Homf ` Q ) C_ V )
50 8 37 6 34 13 49 hofcl 
 |-  ( ph -> H e. ( ( ( oppCat ` Q ) Xc. Q ) Func T ) )
51 16 17 opelxpd 
 |-  ( ph -> <. F , X >. e. ( ( O Func S ) X. B ) )
52 25 48 50 51 cofu1 
 |-  ( ph -> ( ( 1st ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) ` <. F , X >. ) = ( ( 1st ` H ) ` ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ) )
53 21 52 syl5eq 
 |-  ( ph -> ( F ( 1st ` Z ) X ) = ( ( 1st ` H ) ` ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ) )
54 eqid 
 |-  ( Hom ` ( Q Xc. O ) ) = ( Hom ` ( Q Xc. O ) )
55 26 25 54 45 47 51 prf1 
 |-  ( ph -> ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) = <. ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. F , X >. ) , ( ( 1st ` ( Q 1stF O ) ) ` <. F , X >. ) >. )
56 25 36 44 51 cofu1 
 |-  ( ph -> ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. F , X >. ) = ( ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ` ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ) )
57 fvex 
 |-  ( 1st ` Y ) e. _V
58 fvex 
 |-  ( 2nd ` Y ) e. _V
59 58 tposex 
 |-  tpos ( 2nd ` Y ) e. _V
60 57 59 op1st 
 |-  ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) = ( 1st ` Y )
61 60 a1i 
 |-  ( ph -> ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) = ( 1st ` Y ) )
62 22 25 54 34 29 35 51 2ndf1 
 |-  ( ph -> ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) = ( 2nd ` <. F , X >. ) )
63 op2ndg 
 |-  ( ( F e. ( O Func S ) /\ X e. B ) -> ( 2nd ` <. F , X >. ) = X )
64 16 17 63 syl2anc 
 |-  ( ph -> ( 2nd ` <. F , X >. ) = X )
65 62 64 eqtrd 
 |-  ( ph -> ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) = X )
66 61 65 fveq12d 
 |-  ( ph -> ( ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ` ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ) = ( ( 1st ` Y ) ` X ) )
67 56 66 eqtrd 
 |-  ( ph -> ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. F , X >. ) = ( ( 1st ` Y ) ` X ) )
68 22 25 54 34 29 46 51 1stf1 
 |-  ( ph -> ( ( 1st ` ( Q 1stF O ) ) ` <. F , X >. ) = ( 1st ` <. F , X >. ) )
69 op1stg 
 |-  ( ( F e. ( O Func S ) /\ X e. B ) -> ( 1st ` <. F , X >. ) = F )
70 16 17 69 syl2anc 
 |-  ( ph -> ( 1st ` <. F , X >. ) = F )
71 68 70 eqtrd 
 |-  ( ph -> ( ( 1st ` ( Q 1stF O ) ) ` <. F , X >. ) = F )
72 67 71 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. F , X >. ) , ( ( 1st ` ( Q 1stF O ) ) ` <. F , X >. ) >. = <. ( ( 1st ` Y ) ` X ) , F >. )
73 55 72 eqtrd 
 |-  ( ph -> ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) = <. ( ( 1st ` Y ) ` X ) , F >. )
74 73 fveq2d 
 |-  ( ph -> ( ( 1st ` H ) ` ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ) = ( ( 1st ` H ) ` <. ( ( 1st ` Y ) ` X ) , F >. ) )
75 df-ov 
 |-  ( ( ( 1st ` Y ) ` X ) ( 1st ` H ) F ) = ( ( 1st ` H ) ` <. ( ( 1st ` Y ) ` X ) , F >. )
76 74 75 eqtr4di 
 |-  ( ph -> ( ( 1st ` H ) ` ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ) = ( ( ( 1st ` Y ) ` X ) ( 1st ` H ) F ) )
77 eqid 
 |-  ( O Nat S ) = ( O Nat S )
78 7 77 fuchom 
 |-  ( O Nat S ) = ( Hom ` Q )
79 1 2 12 17 4 5 31 14 yon1cl 
 |-  ( ph -> ( ( 1st ` Y ) ` X ) e. ( O Func S ) )
80 8 34 23 78 79 16 hof1 
 |-  ( ph -> ( ( ( 1st ` Y ) ` X ) ( 1st ` H ) F ) = ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )
81 53 76 80 3eqtrd 
 |-  ( ph -> ( F ( 1st ` Z ) X ) = ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )