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

Theorem funcrcl 15269
Description: Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)
Assertion
Ref Expression
funcrcl  |-  ( F  e.  ( D  Func  E )  ->  ( D  e.  Cat  /\  E  e. 
Cat ) )

Proof of Theorem funcrcl
Dummy variables  f 
b  g  m  n  t  u  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-func 15264 . 2  |-  Func  =  ( t  e.  Cat ,  u  e.  Cat  |->  {
<. f ,  g >.  |  [. ( Base `  t
)  /  b ]. ( f : b --> ( Base `  u
)  /\  g  e.  X_ z  e.  ( b  X.  b ) ( ( ( f `  ( 1st `  z ) ) ( Hom  `  u
) ( f `  ( 2nd `  z ) ) )  ^m  (
( Hom  `  t ) `
 z ) )  /\  A. x  e.  b  ( ( ( x g x ) `
 ( ( Id
`  t ) `  x ) )  =  ( ( Id `  u ) `  (
f `  x )
)  /\  A. y  e.  b  A. z  e.  b  A. m  e.  ( x ( Hom  `  t ) y ) A. n  e.  ( y ( Hom  `  t
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  t )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  u )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) } )
21elmpt2cl 6416 1  |-  ( F  e.  ( D  Func  E )  ->  ( D  e.  Cat  /\  E  e. 
Cat ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971    = wceq 1399    e. wcel 1826   A.wral 2732   [.wsbc 3252   <.cop 3950   {copab 4424    X. cxp 4911   -->wf 5492   ` cfv 5496  (class class class)co 6196   1stc1st 6697   2ndc2nd 6698    ^m cmap 7338   X_cixp 7388   Basecbs 14634   Hom chom 14713  compcco 14714   Catccat 15071   Idccid 15072    Func cfunc 15260
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-xp 4919  df-dm 4923  df-iota 5460  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-func 15264
This theorem is referenced by:  funcf1  15272  funcixp  15273  funcid  15276  funcco  15277  funcsect  15278  funcinv  15279  funciso  15280  funcoppc  15281  cofucl  15294  cofulid  15296  cofurid  15297  funcres  15302  funcres2b  15303  funcpropd  15306  funcres2c  15307  isfull  15316  isfth  15320  fthsect  15331  fthinv  15332  fthmon  15333  fthepi  15334  ffthiso  15335  natfval  15352  fucbas  15366  fuchom  15367  fucco  15368  fuccocl  15370  fucidcl  15371  fuclid  15372  fucrid  15373  fucass  15374  fucid  15377  fucsect  15378  fucinv  15379  invfuc  15380  fuciso  15381  funcsetcres2  15489  prfcl  15589  prf1st  15590  prf2nd  15591  curf1cl  15614  curfcl  15618  uncfval  15620  uncfcl  15621  uncf1  15622  uncf2  15623  curfuncf  15624  uncfcurf  15625  yonffthlem  15668  yoneda  15669
  Copyright terms: Public domain W3C validator