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 16387
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 16384 . 2 class cat
2 vc . . 3 setvar 𝑐
3 vh . . 3 setvar
4 cvv 3191 . . 3 class V
52cv 1479 . . . . 5 class 𝑐
63cv 1479 . . . . . . 7 class
76cdm 5079 . . . . . 6 class dom
87cdm 5079 . . . . 5 class dom dom
9 cress 15777 . . . . 5 class s
105, 8, 9co 6605 . . . 4 class (𝑐s dom dom )
11 cnx 15773 . . . . . 6 class ndx
12 chom 15868 . . . . . 6 class Hom
1311, 12cfv 5850 . . . . 5 class (Hom ‘ndx)
1413, 6cop 4159 . . . 4 class ⟨(Hom ‘ndx),
15 csts 15774 . . . 4 class sSet
1610, 14, 15co 6605 . . 3 class ((𝑐s dom dom ) sSet ⟨(Hom ‘ndx), ⟩)
172, 3, 4, 4, 16cmpt2 6607 . 2 class (𝑐 ∈ V, ∈ V ↦ ((𝑐s dom dom ) sSet ⟨(Hom ‘ndx), ⟩))
181, 17wceq 1480 1 wff cat = (𝑐 ∈ V, ∈ V ↦ ((𝑐s dom dom ) sSet ⟨(Hom ‘ndx), ⟩))
Colors of variables: wff setvar class
This definition is referenced by:  rescval  16403
  Copyright terms: Public domain W3C validator