Definition df-resf 16521

Description: Define the restriction of a functor to a subcategory (analogue of df-res 5126). (Contributed by Mario Carneiro, 6-Jan-2017.)

Assertion

Ref	Expression
df-resf	|- |`f = ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. )

Distinct variable group:   f, h, x

Detailed syntax breakdown of Definition df-resf

Step	Hyp	Ref	Expression
1		cresf 16517	. 2 class |`f
2		vf	. . 3 setvar f
3		vh	. . 3 setvar h
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . . 6 class f
6		c1st 7166	. . . . . 6 class 1st
7	5, 6	cfv 5888	. . . . 5 class ( 1st ` f )
8	3	cv 1482	. . . . . . 7 class h
9	8	cdm 5114	. . . . . 6 class dom h
10	9	cdm 5114	. . . . 5 class dom dom h
11	7, 10	cres 5116	. . . 4 class ( ( 1st ` f ) |` dom dom h )
12		vx	. . . . 5 setvar x
13	12	cv 1482	. . . . . . 7 class x
14		c2nd 7167	. . . . . . . 8 class 2nd
15	5, 14	cfv 5888	. . . . . . 7 class ( 2nd ` f )
16	13, 15	cfv 5888	. . . . . 6 class ( ( 2nd ` f ) ` x )
17	13, 8	cfv 5888	. . . . . 6 class ( h ` x )
18	16, 17	cres 5116	. . . . 5 class ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) )
19	12, 9, 18	cmpt 4729	. . . 4 class ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) )
20	11, 19	cop 4183	. . 3 class <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >.
21	2, 3, 4, 4, 20	cmpt2 6652	. 2 class ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. )
22	1, 21	wceq 1483	1 wff |`f = ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. )

This definition is referenced by:  resfval  16552