Definition df-resc 16471

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 = ( c e. _V , h e. _V |-> ( ( c ↾s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) )

Distinct variable group:   h, c

Detailed syntax breakdown of Definition df-resc

Step	Hyp	Ref	Expression
1		cresc 16468	. 2 class |`cat
2		vc	. . 3 setvar c
3		vh	. . 3 setvar h
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . 5 class c
6	3	cv 1482	. . . . . . 7 class h
7	6	cdm 5114	. . . . . 6 class dom h
8	7	cdm 5114	. . . . 5 class dom dom h
9		cress 15858	. . . . 5 class ↾s
10	5, 8, 9	co 6650	. . . 4 class ( c ↾s dom dom h )
11		cnx 15854	. . . . . 6 class ndx
12		chom 15952	. . . . . 6 class Hom
13	11, 12	cfv 5888	. . . . 5 class ( Hom ` ndx )
14	13, 6	cop 4183	. . . 4 class <. ( Hom ` ndx ) , h >.
15		csts 15855	. . . 4 class sSet
16	10, 14, 15	co 6650	. . 3 class ( ( c ↾s dom dom h ) sSet <. ( Hom ` ndx ) , h >. )
17	2, 3, 4, 4, 16	cmpt2 6652	. 2 class ( c e. _V , h e. _V |-> ( ( c ↾s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) )
18	1, 17	wceq 1483	1 wff |`cat = ( c e. _V , h e. _V |-> ( ( c ↾s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) )

This definition is referenced by:  rescval  16487