This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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