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

Definition df-resc 15044
Description: Define the restriction of a category to a given set of arrows. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
df-resc  |-  |`cat  =  (
c  e.  _V ,  h  e.  _V  |->  ( ( cs 
dom  dom  h ) sSet  <. ( Hom  `  ndx ) ,  h >. ) )
Distinct variable group:    h, c

Detailed syntax breakdown of Definition df-resc
StepHypRef Expression
1 cresc 15041 . 2  class  |`cat
2 vc . . 3  setvar  c
3 vh . . 3  setvar  h
4 cvv 3113 . . 3  class  _V
52cv 1378 . . . . 5  class  c
63cv 1378 . . . . . . 7  class  h
76cdm 4999 . . . . . 6  class  dom  h
87cdm 4999 . . . . 5  class  dom  dom  h
9 cress 14494 . . . . 5  classs
105, 8, 9co 6285 . . . 4  class  ( cs  dom 
dom  h )
11 cnx 14490 . . . . . 6  class  ndx
12 chom 14569 . . . . . 6  class  Hom
1311, 12cfv 5588 . . . . 5  class  ( Hom  `  ndx )
1413, 6cop 4033 . . . 4  class  <. ( Hom  `  ndx ) ,  h >.
15 csts 14491 . . . 4  class sSet
1610, 14, 15co 6285 . . 3  class  ( ( cs 
dom  dom  h ) sSet  <. ( Hom  `  ndx ) ,  h >. )
172, 3, 4, 4, 16cmpt2 6287 . 2  class  ( c  e.  _V ,  h  e.  _V  |->  ( ( cs  dom 
dom  h ) sSet  <. ( Hom  `  ndx ) ,  h >. ) )
181, 17wceq 1379 1  wff  |`cat  =  (
c  e.  _V ,  h  e.  _V  |->  ( ( cs 
dom  dom  h ) sSet  <. ( Hom  `  ndx ) ,  h >. ) )
Colors of variables: wff setvar class
This definition is referenced by:  rescval  15060
  Copyright terms: Public domain W3C validator