Definition df-resc 17966

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

Step	Hyp	Ref	Expression
1		cresc 17963	. 2 class ↾cat
2		vc	. . 3 setvar 𝑐
3		vh	. . 3 setvar ℎ
4		cvv 3451	. . 3 class V
5	2	cv 1569	. . . . 5 class 𝑐
6	3	cv 1569	. . . . . . 7 class ℎ
7	6	cdm 5651	. . . . . 6 class dom ℎ
8	7	cdm 5651	. . . . 5 class dom dom ℎ
9		cress 17388	. . . . 5 class ↾s
10	5, 8, 9	co 7412	. . . 4 class (𝑐 ↾s dom dom ℎ)
11		cnx 17351	. . . . . 6 class ndx
12		chom 17419	. . . . . 6 class Hom
13	11, 12	cfv 6531	. . . . 5 class (Hom ‘ndx)
14	13, 6	cop 4590	. . . 4 class ⟨(Hom ‘ndx), ℎ⟩
15		csts 17321	. . . 4 class sSet
16	10, 14, 15	co 7412	. . 3 class ((𝑐 ↾s dom dom ℎ) sSet ⟨(Hom ‘ndx), ℎ⟩)
17	2, 3, 4, 4, 16	cmpo 7414	. 2 class (𝑐 ∈ V, ℎ ∈ V ↦ ((𝑐 ↾s dom dom ℎ) sSet ⟨(Hom ‘ndx), ℎ⟩))
18	1, 17	wceq 1570	1 wff ↾cat = (𝑐 ∈ V, ℎ ∈ V ↦ ((𝑐 ↾s dom dom ℎ) sSet ⟨(Hom ‘ndx), ℎ⟩))

This definition is used by:  rescval  17982  resccat  50126