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

Theorem fucval 13881
Description: Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
fucval.q  |-  Q  =  ( C FuncCat  D )
fucval.b  |-  B  =  ( C  Func  D
)
fucval.n  |-  N  =  ( C Nat  D )
fucval.a  |-  A  =  ( Base `  C
)
fucval.o  |-  .x.  =  (comp `  D )
fucval.c  |-  ( ph  ->  C  e.  Cat )
fucval.d  |-  ( ph  ->  D  e.  Cat )
fucval.x  |-  ( ph  -> 
.xb  =  ( v  e.  ( B  X.  B ) ,  h  e.  B  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g N h ) ,  a  e.  ( f N g ) 
|->  ( x  e.  A  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) ( a `  x ) ) ) ) ) )
Assertion
Ref Expression
fucval  |-  ( ph  ->  Q  =  { <. (
Base `  ndx ) ,  B >. ,  <. (  Hom  `  ndx ) ,  N >. ,  <. (comp ` 
ndx ) ,  .xb  >. } )
Distinct variable groups:    v, h, B    a, b, f, g, h, v, x, ph    C, a, b, f, g, h, v, x    D, a, b, f, g, h, v, x
Allowed substitution hints:    A( x, v, f, g, h, a, b)    B( x, f, g, a, b)    Q( x, v, f, g, h, a, b)    .xb ( x, v, f, g, h, a, b)    .x. ( x, v, f, g, h, a, b)    N( x, v, f, g, h, a, b)

Proof of Theorem fucval
Dummy variables  t  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fucval.q . 2  |-  Q  =  ( C FuncCat  D )
2 df-fuc 13867 . . . 4  |- FuncCat  =  ( t  e.  Cat ,  u  e.  Cat  |->  { <. (
Base `  ndx ) ,  ( t  Func  u
) >. ,  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
32a1i 10 . . 3  |-  ( ph  -> FuncCat 
=  ( t  e. 
Cat ,  u  e.  Cat  |->  { <. ( Base `  ndx ) ,  ( t  Func  u
) >. ,  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } ) )
4 simprl 732 . . . . . . 7  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
t  =  C )
5 simprr 733 . . . . . . 7  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  ->  u  =  D )
64, 5oveq12d 5918 . . . . . 6  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( t  Func  u
)  =  ( C 
Func  D ) )
7 fucval.b . . . . . 6  |-  B  =  ( C  Func  D
)
86, 7syl6eqr 2366 . . . . 5  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( t  Func  u
)  =  B )
98opeq2d 3840 . . . 4  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  ->  <. ( Base `  ndx ) ,  ( t  Func  u ) >.  =  <. (
Base `  ndx ) ,  B >. )
104, 5oveq12d 5918 . . . . . 6  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( t Nat  u )  =  ( C Nat  D
) )
11 fucval.n . . . . . 6  |-  N  =  ( C Nat  D )
1210, 11syl6eqr 2366 . . . . 5  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( t Nat  u )  =  N )
1312opeq2d 3840 . . . 4  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  ->  <. (  Hom  `  ndx ) ,  ( t Nat  u ) >.  =  <. (  Hom  `  ndx ) ,  N >. )
148, 8xpeq12d 4751 . . . . . . 7  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( ( t  Func  u )  X.  ( t 
Func  u ) )  =  ( B  X.  B
) )
1512oveqd 5917 . . . . . . . . . 10  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( g ( t Nat  u ) h )  =  ( g N h ) )
1612oveqd 5917 . . . . . . . . . 10  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( f ( t Nat  u ) g )  =  ( f N g ) )
174fveq2d 5567 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( Base `  t )  =  ( Base `  C
) )
18 fucval.a . . . . . . . . . . . 12  |-  A  =  ( Base `  C
)
1917, 18syl6eqr 2366 . . . . . . . . . . 11  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( Base `  t )  =  A )
205fveq2d 5567 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
(comp `  u )  =  (comp `  D )
)
21 fucval.o . . . . . . . . . . . . . 14  |-  .x.  =  (comp `  D )
2220, 21syl6eqr 2366 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
(comp `  u )  =  .x.  )
2322oveqd 5917 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  u )
( ( 1st `  h
) `  x )
)  =  ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) )
2423oveqd 5917 . . . . . . . . . . 11  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) )  =  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) ( a `  x ) ) )
2519, 24mpteq12dv 4135 . . . . . . . . . 10  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( x  e.  (
Base `  t )  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) )  =  ( x  e.  A  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.  .x.  ( ( 1st `  h
) `  x )
) ( a `  x ) ) ) )
2615, 16, 25mpt2eq123dv 5952 . . . . . . . . 9  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  ( b  e.  ( g N h ) ,  a  e.  ( f N g )  |->  ( x  e.  A  |->  ( ( b `  x
) ( <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) ( a `  x ) ) ) ) )
2726csbeq2dv 3140 . . . . . . . 8  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  ->  [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 2nd `  v )  /  g ]_ (
b  e.  ( g N h ) ,  a  e.  ( f N g )  |->  ( x  e.  A  |->  ( ( b `  x
) ( <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) ( a `  x ) ) ) ) )
2827csbeq2dv 3140 . . . . . . 7  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  ->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 1st `  v )  /  f ]_ [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g N h ) ,  a  e.  ( f N g )  |->  ( x  e.  A  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) ( a `  x ) ) ) ) )
2914, 8, 28mpt2eq123dv 5952 . . . . . 6  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( v  e.  ( ( t  Func  u
)  X.  ( t 
Func  u ) ) ,  h  e.  ( t 
Func  u )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )  =  ( v  e.  ( B  X.  B ) ,  h  e.  B  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g N h ) ,  a  e.  ( f N g ) 
|->  ( x  e.  A  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) ( a `  x ) ) ) ) ) )
30 fucval.x . . . . . . 7  |-  ( ph  -> 
.xb  =  ( v  e.  ( B  X.  B ) ,  h  e.  B  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g N h ) ,  a  e.  ( f N g ) 
|->  ( x  e.  A  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) ( a `  x ) ) ) ) ) )
3130adantr 451 . . . . . 6  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  ->  .xb  =  ( v  e.  ( B  X.  B
) ,  h  e.  B  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g N h ) ,  a  e.  ( f N g ) 
|->  ( x  e.  A  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.  .x.  ( ( 1st `  h ) `  x ) ) ( a `  x ) ) ) ) ) )
3229, 31eqtr4d 2351 . . . . 5  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  -> 
( v  e.  ( ( t  Func  u
)  X.  ( t 
Func  u ) ) ,  h  e.  ( t 
Func  u )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )  = 
.xb  )
3332opeq2d 3840 . . . 4  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  ->  <. (comp `  ndx ) ,  ( v  e.  ( ( t  Func  u
)  X.  ( t 
Func  u ) ) ,  h  e.  ( t 
Func  u )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >.  =  <. (comp `  ndx ) ,  .xb  >. )
349, 13, 33tpeq123d 3755 . . 3  |-  ( (
ph  /\  ( t  =  C  /\  u  =  D ) )  ->  { <. ( Base `  ndx ) ,  ( t  Func  u ) >. ,  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. }  =  { <. ( Base `  ndx ) ,  B >. ,  <. (  Hom  `  ndx ) ,  N >. ,  <. (comp ` 
ndx ) ,  .xb  >. } )
35 fucval.c . . 3  |-  ( ph  ->  C  e.  Cat )
36 fucval.d . . 3  |-  ( ph  ->  D  e.  Cat )
37 tpex 4556 . . . 4  |-  { <. (
Base `  ndx ) ,  B >. ,  <. (  Hom  `  ndx ) ,  N >. ,  <. (comp ` 
ndx ) ,  .xb  >. }  e.  _V
3837a1i 10 . . 3  |-  ( ph  ->  { <. ( Base `  ndx ) ,  B >. , 
<. (  Hom  `  ndx ) ,  N >. , 
<. (comp `  ndx ) , 
.xb  >. }  e.  _V )
393, 34, 35, 36, 38ovmpt2d 6017 . 2  |-  ( ph  ->  ( C FuncCat  D )  =  { <. ( Base `  ndx ) ,  B >. , 
<. (  Hom  `  ndx ) ,  N >. , 
<. (comp `  ndx ) , 
.xb  >. } )
401, 39syl5eq 2360 1  |-  ( ph  ->  Q  =  { <. (
Base `  ndx ) ,  B >. ,  <. (  Hom  `  ndx ) ,  N >. ,  <. (comp ` 
ndx ) ,  .xb  >. } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1633    e. wcel 1701   _Vcvv 2822   [_csb 3115   {ctp 3676   <.cop 3677    e. cmpt 4114    X. cxp 4724   ` cfv 5292  (class class class)co 5900    e. cmpt2 5902   1stc1st 6162   2ndc2nd 6163   ndxcnx 13192   Basecbs 13195    Hom chom 13266  compcco 13267   Catccat 13615    Func cfunc 13777   Nat cnat 13864   FuncCat cfuc 13865
This theorem is referenced by:  fuccofval  13882  fucbas  13883  fuchom  13884  fucpropd  13900  catcfuccl  13990
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-iota 5256  df-fun 5294  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-fuc 13867
  Copyright terms: Public domain W3C validator