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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cresc	|- |`cat
1		vc	|- c
2		cvv	|- _V
3		vh	|- h
4	1	cv	|- c
5		cress	|- |`s
6	3	cv	|- h
7	6	cdm	|- dom h
8	7	cdm	|- dom dom h
9	4 8 5	co	|- ( c |`s dom dom h )
10		csts	|- sSet
11		chom	|- Hom
12		cnx	|- ndx
13	12 11	cfv	|- ( Hom ` ndx )
14	13 6	cop	|- <. ( Hom ` ndx ) , h >.
15	9 14 10	co	|- ( ( c |`s dom dom h ) sSet <. ( Hom ` ndx ) , h >. )
16	1 3 2 2 15	cmpo	|- ( c e. _V , h e. _V |-> ( ( c |`s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) )
17	0 16	wceq	|- |`cat = ( c e. _V , h e. _V |-> ( ( c |`s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) )