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

Definition df-resc 13704
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 13701 . 2  class  |`cat
2 vc . . 3  set  c
3 vh . . 3  set  h
4 cvv 2801 . . 3  class  _V
52cv 1631 . . . . 5  class  c
63cv 1631 . . . . . . 7  class  h
76cdm 4705 . . . . . 6  class  dom  h
87cdm 4705 . . . . 5  class  dom  dom  h
9 cress 13165 . . . . 5  classs
105, 8, 9co 5874 . . . 4  class  ( cs  dom 
dom  h )
11 cnx 13161 . . . . . 6  class  ndx
12 chom 13235 . . . . . 6  class  Hom
1311, 12cfv 5271 . . . . 5  class  (  Hom  `  ndx )
1413, 6cop 3656 . . . 4  class  <. (  Hom  `  ndx ) ,  h >.
15 csts 13162 . . . 4  class sSet
1610, 14, 15co 5874 . . 3  class  ( ( cs 
dom  dom  h ) sSet  <. (  Hom  `  ndx ) ,  h >. )
172, 3, 4, 4, 16cmpt2 5876 . 2  class  ( c  e.  _V ,  h  e.  _V  |->  ( ( cs  dom 
dom  h ) sSet  <. (  Hom  `  ndx ) ,  h >. ) )
181, 17wceq 1632 1  wff  |`cat  =  (
c  e.  _V ,  h  e.  _V  |->  ( ( cs 
dom  dom  h ) sSet  <. (  Hom  `  ndx ) ,  h >. ) )
Colors of variables: wff set class
This definition is referenced by:  rescval  13720
  Copyright terms: Public domain W3C validator