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

Theorem relfunc 15353
Description: The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
relfunc  |-  Rel  ( D  Func  E )

Proof of Theorem relfunc
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 15349 . 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 ) ) ) ) } )
21relmpt2opab 6855 1  |-  Rel  ( D  Func  E )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823   A.wral 2804   [.wsbc 3324   <.cop 4022    X. cxp 4986   Rel wrel 4993   -->wf 5566   ` cfv 5570  (class class class)co 6270   1stc1st 6771   2ndc2nd 6772    ^m cmap 7412   X_cixp 7462   Basecbs 14719   Hom chom 14798  compcco 14799   Catccat 15156   Idccid 15157    Func cfunc 15345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-1st 6773  df-2nd 6774  df-func 15349
This theorem is referenced by:  cofuval  15373  cofu1  15375  cofu2  15377  cofuval2  15378  cofucl  15379  cofuass  15380  cofulid  15381  cofurid  15382  funcres  15387  funcres2  15389  wunfunc  15390  funcpropd  15391  relfull  15399  relfth  15400  isfull  15401  isfth  15405  idffth  15424  cofull  15425  cofth  15426  ressffth  15429  isnat  15438  isnat2  15439  nat1st2nd  15442  fuccocl  15455  fucidcl  15456  fuclid  15457  fucrid  15458  fucass  15459  fucsect  15463  fucinv  15464  invfuc  15465  fuciso  15466  natpropd  15467  fucpropd  15468  catciso  15588  prfval  15670  prfcl  15674  prf1st  15675  prf2nd  15676  1st2ndprf  15677  evlfcllem  15692  evlfcl  15693  curf1cl  15699  curf2cl  15702  curfcl  15703  uncf1  15707  uncf2  15708  curfuncf  15709  uncfcurf  15710  diag1cl  15713  diag2cl  15717  curf2ndf  15718  yon1cl  15734  oyon1cl  15742  yonedalem1  15743  yonedalem21  15744  yonedalem3a  15745  yonedalem4c  15748  yonedalem22  15749  yonedalem3b  15750  yonedalem3  15751  yonedainv  15752  yonffthlem  15753  yoniso  15756
  Copyright terms: Public domain W3C validator