Definition df-resf

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cresf	|- |`f
1		vf	|- f
2		cvv	|- _V
3		vh	|- h
4		c1st	|- 1st
5	1	cv	|- f
6	5 4	cfv	|- ( 1st ` f )
7	3	cv	|- h
8	7	cdm	|- dom h
9	8	cdm	|- dom dom h
10	6 9	cres	|- ( ( 1st ` f ) |` dom dom h )
11		vx	|- x
12		c2nd	|- 2nd
13	5 12	cfv	|- ( 2nd ` f )
14	11	cv	|- x
15	14 13	cfv	|- ( ( 2nd ` f ) ` x )
16	14 7	cfv	|- ( h ` x )
17	15 16	cres	|- ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) )
18	11 8 17	cmpt	|- ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) )
19	10 18	cop	|- <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >.
20	1 3 2 2 19	cmpo	|- ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. )
21	0 20	wceq	|- |`f = ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. )