Metamath Proof Explorer

Definition df-resc

Description: Define the restriction of a category to a given set of arrows. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Assertion df-resc ⊢ ↾ cat = c ∈ V , h ∈ V ⟼ c ↾ 𝑠 dom ⁡ dom ⁡ h sSet Hom ⁡ ndx h

Detailed syntax breakdown

Step Hyp Ref Expression
0 cresc class ↾ cat
1 vc setvar c
2 cvv class V
3 vh setvar h
4 1 cv setvar c
5 cress class ↾ 𝑠
6 3 cv setvar h
7 6 cdm class dom ⁡ h
8 7 cdm class dom ⁡ dom ⁡ h
9 4 8 5 co class c ↾ 𝑠 dom ⁡ dom ⁡ h
10 csts class sSet
11 chom class Hom
12 cnx class ndx
13 12 11 cfv class Hom ⁡ ndx
14 13 6 cop class Hom ⁡ ndx h
15 9 14 10 co class c ↾ 𝑠 dom ⁡ dom ⁡ h sSet Hom ⁡ ndx h
16 1 3 2 2 15 cmpo class c ∈ V , h ∈ V ⟼ c ↾ 𝑠 dom ⁡ dom ⁡ h sSet Hom ⁡ ndx h
17 0 16 wceq wff ↾ cat = c ∈ V , h ∈ V ⟼ c ↾ 𝑠 dom ⁡ dom ⁡ h sSet Hom ⁡ ndx h