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

Definition df-resc 17757
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 = (𝑐 ∈ V, β„Ž ∈ V ↦ ((𝑐 β†Ύs dom dom β„Ž) sSet ⟨(Hom β€˜ndx), β„ŽβŸ©))
Distinct variable group:   β„Ž,𝑐

Detailed syntax breakdown of Definition df-resc
StepHypRef Expression
1 cresc 17754 . 2 class β†Ύcat
2 vc . . 3 setvar 𝑐
3 vh . . 3 setvar β„Ž
4 cvv 3474 . . 3 class V
52cv 1540 . . . . 5 class 𝑐
63cv 1540 . . . . . . 7 class β„Ž
76cdm 5676 . . . . . 6 class dom β„Ž
87cdm 5676 . . . . 5 class dom dom β„Ž
9 cress 17172 . . . . 5 class β†Ύs
105, 8, 9co 7408 . . . 4 class (𝑐 β†Ύs dom dom β„Ž)
11 cnx 17125 . . . . . 6 class ndx
12 chom 17207 . . . . . 6 class Hom
1311, 12cfv 6543 . . . . 5 class (Hom β€˜ndx)
1413, 6cop 4634 . . . 4 class ⟨(Hom β€˜ndx), β„ŽβŸ©
15 csts 17095 . . . 4 class sSet
1610, 14, 15co 7408 . . 3 class ((𝑐 β†Ύs dom dom β„Ž) sSet ⟨(Hom β€˜ndx), β„ŽβŸ©)
172, 3, 4, 4, 16cmpo 7410 . 2 class (𝑐 ∈ V, β„Ž ∈ V ↦ ((𝑐 β†Ύs dom dom β„Ž) sSet ⟨(Hom β€˜ndx), β„ŽβŸ©))
181, 17wceq 1541 1 wff β†Ύcat = (𝑐 ∈ V, β„Ž ∈ V ↦ ((𝑐 β†Ύs dom dom β„Ž) sSet ⟨(Hom β€˜ndx), β„ŽβŸ©))
Colors of variables: wff setvar class
This definition is referenced by:  rescval  17773
  Copyright terms: Public domain W3C validator