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

Definition df-resc 14736
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 14733 . 2  class  |`cat
2 vc . . 3  setvar  c
3 vh . . 3  setvar  h
4 cvv 2984 . . 3  class  _V
52cv 1368 . . . . 5  class  c
63cv 1368 . . . . . . 7  class  h
76cdm 4852 . . . . . 6  class  dom  h
87cdm 4852 . . . . 5  class  dom  dom  h
9 cress 14187 . . . . 5  classs
105, 8, 9co 6103 . . . 4  class  ( cs  dom 
dom  h )
11 cnx 14183 . . . . . 6  class  ndx
12 chom 14261 . . . . . 6  class  Hom
1311, 12cfv 5430 . . . . 5  class  ( Hom  `  ndx )
1413, 6cop 3895 . . . 4  class  <. ( Hom  `  ndx ) ,  h >.
15 csts 14184 . . . 4  class sSet
1610, 14, 15co 6103 . . 3  class  ( ( cs 
dom  dom  h ) sSet  <. ( Hom  `  ndx ) ,  h >. )
172, 3, 4, 4, 16cmpt2 6105 . 2  class  ( c  e.  _V ,  h  e.  _V  |->  ( ( cs  dom 
dom  h ) sSet  <. ( Hom  `  ndx ) ,  h >. ) )
181, 17wceq 1369 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  14752
  Copyright terms: Public domain W3C validator