MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  yonedalem4b Unicode version

Theorem yonedalem4b 14052
Description: Lemma for yoneda 14059. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
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  X.c  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 ) ) ⟨,⟩F  ( 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
Ref Expression
yonedalem4b  |-  ( ph  ->  ( ( ( ( F N X ) `
 A ) `  P ) `  G
)  =  ( ( ( X ( 2nd `  F ) P ) `
 G ) `  A ) )
Distinct variable groups:    f, g, x, y,  .1.    u, g, A, y    u, f, C, g, x, y   
f, E, g, u, y    f, F, g, u, x, y    B, f, g, u, x, y   
f, G, g, x, y    f, O, g, u, x, y    S, f, g, u, x, y    Q, f, g, u, x    T, f, g, u, y    P, f, g, x, y    ph, f, g, u, x, y    u, R    f, Y, g, u, x, y   
f, Z, g, u, x, y    f, X, g, u, x, y
Allowed substitution hints:    A( x, f)    P( u)    Q( y)    R( x, y, f, g)    T( x)    U( x, y, u, f, g)    .1. ( u)    E( x)    G( u)    H( x, y, u, f, g)    N( x, y, u, f, g)    V( x, y, u, f, g)    W( x, y, u, f, g)

Proof of Theorem yonedalem4b
StepHypRef Expression
1 yoneda.y . . . . 5  |-  Y  =  (Yon `  C )
2 yoneda.b . . . . 5  |-  B  =  ( Base `  C
)
3 yoneda.1 . . . . 5  |-  .1.  =  ( Id `  C )
4 yoneda.o . . . . 5  |-  O  =  (oppCat `  C )
5 yoneda.s . . . . 5  |-  S  =  ( SetCat `  U )
6 yoneda.t . . . . 5  |-  T  =  ( SetCat `  V )
7 yoneda.q . . . . 5  |-  Q  =  ( O FuncCat  S )
8 yoneda.h . . . . 5  |-  H  =  (HomF
`  Q )
9 yoneda.r . . . . 5  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
10 yoneda.e . . . . 5  |-  E  =  ( O evalF  S )
11 yoneda.z . . . . 5  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
12 yoneda.c . . . . 5  |-  ( ph  ->  C  e.  Cat )
13 yoneda.w . . . . 5  |-  ( ph  ->  V  e.  W )
14 yoneda.u . . . . 5  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
15 yoneda.v . . . . 5  |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U
)  C_  V )
16 yonedalem21.f . . . . 5  |-  ( ph  ->  F  e.  ( O 
Func  S ) )
17 yonedalem21.x . . . . 5  |-  ( ph  ->  X  e.  B )
18 yonedalem4.n . . . . 5  |-  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 . . . . 5  |-  ( ph  ->  A  e.  ( ( 1st `  F ) `
 X ) )
201, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19yonedalem4a 14051 . . . 4  |-  ( ph  ->  ( ( F N X ) `  A
)  =  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) y ) `
 g ) `  A ) ) ) )
2120fveq1d 5529 . . 3  |-  ( ph  ->  ( ( ( F N X ) `  A ) `  P
)  =  ( ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) y ) `  g
) `  A )
) ) `  P
) )
2221fveq1d 5529 . 2  |-  ( ph  ->  ( ( ( ( F N X ) `
 A ) `  P ) `  G
)  =  ( ( ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) y ) `  g
) `  A )
) ) `  P
) `  G )
)
23 eqidd 2286 . . 3  |-  ( 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 )
) ) )
24 yonedalem4b.p . . . 4  |-  ( ph  ->  P  e.  B )
25 ovex 5885 . . . . . 6  |-  ( y (  Hom  `  C
) X )  e. 
_V
2625mptex 5748 . . . . 5  |-  ( g  e.  ( y (  Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) y ) `
 g ) `  A ) )  e. 
_V
2726a1i 10 . . . 4  |-  ( (
ph  /\  y  =  P )  ->  (
g  e.  ( y (  Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) y ) `  g
) `  A )
)  e.  _V )
28 yonedalem4b.g . . . . . . 7  |-  ( ph  ->  G  e.  ( P (  Hom  `  C
) X ) )
2928adantr 451 . . . . . 6  |-  ( (
ph  /\  y  =  P )  ->  G  e.  ( P (  Hom  `  C ) X ) )
30 simpr 447 . . . . . . 7  |-  ( (
ph  /\  y  =  P )  ->  y  =  P )
3130oveq1d 5875 . . . . . 6  |-  ( (
ph  /\  y  =  P )  ->  (
y (  Hom  `  C
) X )  =  ( P (  Hom  `  C ) X ) )
3229, 31eleqtrrd 2362 . . . . 5  |-  ( (
ph  /\  y  =  P )  ->  G  e.  ( y (  Hom  `  C ) X ) )
33 fvex 5541 . . . . . 6  |-  ( ( ( X ( 2nd `  F ) y ) `
 g ) `  A )  e.  _V
3433a1i 10 . . . . 5  |-  ( ( ( ph  /\  y  =  P )  /\  g  =  G )  ->  (
( ( X ( 2nd `  F ) y ) `  g
) `  A )  e.  _V )
35 simplr 731 . . . . . . . 8  |-  ( ( ( ph  /\  y  =  P )  /\  g  =  G )  ->  y  =  P )
3635oveq2d 5876 . . . . . . 7  |-  ( ( ( ph  /\  y  =  P )  /\  g  =  G )  ->  ( X ( 2nd `  F
) y )  =  ( X ( 2nd `  F ) P ) )
37 simpr 447 . . . . . . 7  |-  ( ( ( ph  /\  y  =  P )  /\  g  =  G )  ->  g  =  G )
3836, 37fveq12d 5533 . . . . . 6  |-  ( ( ( ph  /\  y  =  P )  /\  g  =  G )  ->  (
( X ( 2nd `  F ) y ) `
 g )  =  ( ( X ( 2nd `  F ) P ) `  G
) )
3938fveq1d 5529 . . . . 5  |-  ( ( ( ph  /\  y  =  P )  /\  g  =  G )  ->  (
( ( X ( 2nd `  F ) y ) `  g
) `  A )  =  ( ( ( X ( 2nd `  F
) P ) `  G ) `  A
) )
4032, 34, 39fvmptdv2 5615 . . . 4  |-  ( (
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
) ) )
41 nfmpt1 4111 . . . 4  |-  F/_ y
( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) y ) `  g
) `  A )
) )
42 nffvmpt1 5535 . . . . . 6  |-  F/_ y
( ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C ) X ) 
|->  ( ( ( X ( 2nd `  F
) y ) `  g ) `  A
) ) ) `  P )
43 nfcv 2421 . . . . . 6  |-  F/_ y G
4442, 43nffv 5534 . . . . 5  |-  F/_ y
( ( ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) y ) `
 g ) `  A ) ) ) `
 P ) `  G )
4544nfeq1 2430 . . . 4  |-  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 )
4624, 27, 40, 41, 45fvmptdf 5613 . . 3  |-  ( 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 ) ) )
4723, 46mpd 14 . 2  |-  ( ph  ->  ( ( ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) y ) `
 g ) `  A ) ) ) `
 P ) `  G )  =  ( ( ( X ( 2nd `  F ) P ) `  G
) `  A )
)
4822, 47eqtrd 2317 1  |-  ( ph  ->  ( ( ( ( F N X ) `
 A ) `  P ) `  G
)  =  ( ( ( X ( 2nd `  F ) P ) `
 G ) `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1625    e. wcel 1686   _Vcvv 2790    u. cun 3152    C_ wss 3154   <.cop 3645    e. cmpt 4079   ran crn 4692   ` cfv 5257  (class class class)co 5860    e. cmpt2 5862   1stc1st 6122   2ndc2nd 6123  tpos ctpos 6235   Basecbs 13150    Hom chom 13221   Catccat 13568   Idccid 13569    Homf chomf 13570  oppCatcoppc 13616    Func cfunc 13730    o.func ccofu 13732   FuncCat cfuc 13818   SetCatcsetc 13909    X.c cxpc 13944    1stF c1stf 13945    2ndF c2ndf 13946   ⟨,⟩F cprf 13947   evalF cevlf 13985  HomFchof 14024  Yoncyon 14025
This theorem is referenced by:  yonedalem4c  14053  yonedainv  14057
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865
  Copyright terms: Public domain W3C validator