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

Theorem funcrcl 14015
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 14010 . 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 6247 1  |-  ( F  e.  ( D  Func  E )  ->  ( D  e.  Cat  /\  E  e. 
Cat ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721   A.wral 2666   [.wsbc 3121   <.cop 3777   {copab 4225    X. cxp 4835   -->wf 5409   ` cfv 5413  (class class class)co 6040   1stc1st 6306   2ndc2nd 6307    ^m cmap 6977   X_cixp 7022   Basecbs 13424    Hom chom 13495  compcco 13496   Catccat 13844   Idccid 13845    Func cfunc 14006
This theorem is referenced by:  funcf1  14018  funcixp  14019  funcid  14022  funcco  14023  funcsect  14024  funcinv  14025  funciso  14026  funcoppc  14027  cofucl  14040  cofulid  14042  cofurid  14043  funcres  14048  funcres2b  14049  funcpropd  14052  funcres2c  14053  isfull  14062  isfth  14066  fthsect  14077  fthinv  14078  fthmon  14079  fthepi  14080  ffthiso  14081  natfval  14098  fucbas  14112  fuchom  14113  fucco  14114  fuccocl  14116  fucidcl  14117  fuclid  14118  fucrid  14119  fucass  14120  fucid  14123  fucsect  14124  fucinv  14125  invfuc  14126  fuciso  14127  funcsetcres2  14203  prfcl  14255  prf1st  14256  prf2nd  14257  curf1cl  14280  curfcl  14284  uncfval  14286  uncfcl  14287  uncf1  14288  uncf2  14289  curfuncf  14290  uncfcurf  14291  yonffthlem  14334  yoneda  14335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-xp 4843  df-dm 4847  df-iota 5377  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-func 14010
  Copyright terms: Public domain W3C validator