Metamath Proof Explorer

Theorem yonedalem4b

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 29-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 )
yonedalem4.n 
|- N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )
yonedalem4.p 
|- ( ph -> A e. ( ( 1st ` F ) ` X ) )
yonedalem4b.p 
|- ( ph -> P e. B )
yonedalem4b.g 
|- ( ph -> G e. ( P ( Hom ` C ) X ) )
Assertion yonedalem4b 
|- ( ph -> ( ( ( ( F N X ) ` A ) ` P ) ` G ) = ( ( ( X ( 2nd ` F ) P ) ` G ) ` A ) )

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 yonedalem4.n 
 |-  N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )
19 yonedalem4.p 
 |-  ( ph -> A e. ( ( 1st ` F ) ` X ) )
20 yonedalem4b.p 
 |-  ( ph -> P e. B )
21 yonedalem4b.g 
 |-  ( ph -> G e. ( P ( Hom ` C ) X ) )
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 yonedalem4a 
 |-  ( ph -> ( ( F N X ) ` A ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) )
23 22 fveq1d 
 |-  ( ph -> ( ( ( F N X ) ` A ) ` P ) = ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P ) )
24 23 fveq1d 
 |-  ( ph -> ( ( ( ( F N X ) ` A ) ` P ) ` G ) = ( ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P ) ` G ) )
25 eqidd 
 |-  ( ph -> ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) )
26 ovex 
 |-  ( y ( Hom ` C ) X ) e. _V
27 26 mptex 
 |-  ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) e. _V
28 27 a1i 
 |-  ( ( ph /\ y = P ) -> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) e. _V )
29 21 adantr 
 |-  ( ( ph /\ y = P ) -> G e. ( P ( Hom ` C ) X ) )
30 simpr 
 |-  ( ( ph /\ y = P ) -> y = P )
31 30 oveq1d 
 |-  ( ( ph /\ y = P ) -> ( y ( Hom ` C ) X ) = ( P ( Hom ` C ) X ) )
32 29 31 eleqtrrd 
 |-  ( ( ph /\ y = P ) -> G e. ( y ( Hom ` C ) X ) )
33 fvexd 
 |-  ( ( ( ph /\ y = P ) /\ g = G ) -> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) e. _V )
34 simplr 
 |-  ( ( ( ph /\ y = P ) /\ g = G ) -> y = P )
35 34 oveq2d 
 |-  ( ( ( ph /\ y = P ) /\ g = G ) -> ( X ( 2nd ` F ) y ) = ( X ( 2nd ` F ) P ) )
36 simpr 
 |-  ( ( ( ph /\ y = P ) /\ g = G ) -> g = G )
37 35 36 fveq12d 
 |-  ( ( ( ph /\ y = P ) /\ g = G ) -> ( ( X ( 2nd ` F ) y ) ` g ) = ( ( X ( 2nd ` F ) P ) ` G ) )
38 37 fveq1d 
 |-  ( ( ( ph /\ y = P ) /\ g = G ) -> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) = ( ( ( X ( 2nd ` F ) P ) ` G ) ` A ) )
39 32 33 38 fvmptdv2 
 |-  ( ( ph /\ y = P ) -> ( ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P ) = ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) -> ( ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P ) ` G ) = ( ( ( X ( 2nd ` F ) P ) ` G ) ` A ) ) )
40 nfmpt1 
 |-  F/_ y ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) )
41 nffvmpt1 
 |-  F/_ y ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P )
42 nfcv 
 |-  F/_ y G
43 41 42 nffv 
 |-  F/_ y ( ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P ) ` G )
44 43 nfeq1 
 |-  F/ y ( ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P ) ` G ) = ( ( ( X ( 2nd ` F ) P ) ` G ) ` A )
45 20 28 39 40 44 fvmptd2f 
 |-  ( ph -> ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) -> ( ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P ) ` G ) = ( ( ( X ( 2nd ` F ) P ) ` G ) ` A ) ) )
46 25 45 mpd 
 |-  ( ph -> ( ( ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) ` P ) ` G ) = ( ( ( X ( 2nd ` F ) P ) ` G ) ` A ) )
47 24 46 eqtrd 
 |-  ( ph -> ( ( ( ( F N X ) ` A ) ` P ) ` G ) = ( ( ( X ( 2nd ` F ) P ) ` G ) ` A ) )