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 \in V, h \in V ⟼ (c ↾_{𝑠} dom dom h) sSet ⟨Hom (ndx), h⟩)$

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 \in V, h \in V ⟼ (c ↾_{𝑠} dom dom h) sSet ⟨Hom (ndx), h⟩)$
17	0 16	wceq	$wff ↾_{cat} = (c \in V, h \in V ⟼ (c ↾_{𝑠} dom dom h) sSet ⟨Hom (ndx), h⟩)$

Metamath Proof Explorer