Metamath Proof Explorer

Theorem yonedalem4a

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 ) )
Assertion yonedalem4a 
|- ( ph -> ( ( F N X ) ` A ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` 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 18 a1i 
 |-  ( ph -> 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 ) ) ) ) ) )
21 simprl 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> f = F )
22 21 fveq2d 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> ( 1st ` f ) = ( 1st ` F ) )
23 simprr 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> x = X )
24 22 23 fveq12d 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` F ) ` X ) )
25 simplrr 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> x = X )
26 25 oveq2d 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> ( y ( Hom ` C ) x ) = ( y ( Hom ` C ) X ) )
27 simplrl 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> f = F )
28 27 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> ( 2nd ` f ) = ( 2nd ` F ) )
29 eqidd 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> y = y )
30 28 25 29 oveq123d 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> ( x ( 2nd ` f ) y ) = ( X ( 2nd ` F ) y ) )
31 30 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> ( ( x ( 2nd ` f ) y ) ` g ) = ( ( X ( 2nd ` F ) y ) ` g ) )
32 31 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) = ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) )
33 26 32 mpteq12dv 
 |-  ( ( ( ph /\ ( f = F /\ x = X ) ) /\ y e. B ) -> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) = ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) ) )
34 33 mpteq2dva 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) ) ) )
35 24 34 mpteq12dv 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) = ( u e. ( ( 1st ` F ) ` X ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) ) ) ) )
36 fvex 
 |-  ( ( 1st ` F ) ` X ) e. _V
37 36 mptex 
 |-  ( u e. ( ( 1st ` F ) ` X ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) ) ) ) e. _V
38 37 a1i 
 |-  ( ph -> ( u e. ( ( 1st ` F ) ` X ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) ) ) ) e. _V )
39 20 35 16 17 38 ovmpod 
 |-  ( ph -> ( F N X ) = ( u e. ( ( 1st ` F ) ` X ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) ) ) ) )
40 simpr 
 |-  ( ( ph /\ u = A ) -> u = A )
41 40 fveq2d 
 |-  ( ( ph /\ u = A ) -> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) = ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) )
42 41 mpteq2dv 
 |-  ( ( ph /\ u = A ) -> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) ) = ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) )
43 42 mpteq2dv 
 |-  ( ( ph /\ u = A ) -> ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` u ) ) ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) )
44 2 fvexi 
 |-  B e. _V
45 44 mptex 
 |-  ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) e. _V
46 45 a1i 
 |-  ( ph -> ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) e. _V )
47 39 43 19 46 fvmptd 
 |-  ( ph -> ( ( F N X ) ` A ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) )