Metamath Proof Explorer


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 ) ) ) >. )