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

Theorem funcrcl 15090
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 15085 . 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 6501 1  |-  ( F  e.  ( D  Func  E )  ->  ( D  e.  Cat  /\  E  e. 
Cat ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   A.wral 2814   [.wsbc 3331   <.cop 4033   {copab 4504    X. cxp 4997   -->wf 5584   ` cfv 5588  (class class class)co 6284   1stc1st 6782   2ndc2nd 6783    ^m cmap 7420   X_cixp 7469   Basecbs 14490   Hom chom 14566  compcco 14567   Catccat 14919   Idccid 14920    Func cfunc 15081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-xp 5005  df-dm 5009  df-iota 5551  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-func 15085
This theorem is referenced by:  funcf1  15093  funcixp  15094  funcid  15097  funcco  15098  funcsect  15099  funcinv  15100  funciso  15101  funcoppc  15102  cofucl  15115  cofulid  15117  cofurid  15118  funcres  15123  funcres2b  15124  funcpropd  15127  funcres2c  15128  isfull  15137  isfth  15141  fthsect  15152  fthinv  15153  fthmon  15154  fthepi  15155  ffthiso  15156  natfval  15173  fucbas  15187  fuchom  15188  fucco  15189  fuccocl  15191  fucidcl  15192  fuclid  15193  fucrid  15194  fucass  15195  fucid  15198  fucsect  15199  fucinv  15200  invfuc  15201  fuciso  15202  funcsetcres2  15278  prfcl  15330  prf1st  15331  prf2nd  15332  curf1cl  15355  curfcl  15359  uncfval  15361  uncfcl  15362  uncf1  15363  uncf2  15364  curfuncf  15365  uncfcurf  15366  yonffthlem  15409  yoneda  15410
  Copyright terms: Public domain W3C validator