Metamath Proof Explorer

Theorem resfval

Description: Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resfval.c 
|- ( ph -> F e. V )
resfval.d 
|- ( ph -> H e. W )
Assertion resfval 
|- ( ph -> ( F |`f H ) = <. ( ( 1st ` F ) |` dom dom H ) , ( x e. dom H |-> ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) ) >. )

Proof

Step Hyp Ref Expression
1 resfval.c 
 |-  ( ph -> F e. V )
2 resfval.d 
 |-  ( ph -> H e. W )
3 df-resf 
 |-  |`f = ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. )
4 3 a1i 
 |-  ( ph -> |`f = ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. ) )
5 simprl 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> f = F )
6 5 fveq2d 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> ( 1st ` f ) = ( 1st ` F ) )
7 simprr 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> h = H )
8 7 dmeqd 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> dom h = dom H )
9 8 dmeqd 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> dom dom h = dom dom H )
10 6 9 reseq12d 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> ( ( 1st ` f ) |` dom dom h ) = ( ( 1st ` F ) |` dom dom H ) )
11 5 fveq2d 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> ( 2nd ` f ) = ( 2nd ` F ) )
12 11 fveq1d 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> ( ( 2nd ` f ) ` x ) = ( ( 2nd ` F ) ` x ) )
13 7 fveq1d 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> ( h ` x ) = ( H ` x ) )
14 12 13 reseq12d 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) = ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) )
15 8 14 mpteq12dv 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) = ( x e. dom H |-> ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) ) )
16 10 15 opeq12d 
 |-  ( ( ph /\ ( f = F /\ h = H ) ) -> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. = <. ( ( 1st ` F ) |` dom dom H ) , ( x e. dom H |-> ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) ) >. )
17 1 elexd 
 |-  ( ph -> F e. _V )
18 2 elexd 
 |-  ( ph -> H e. _V )
19 opex 
 |-  <. ( ( 1st ` F ) |` dom dom H ) , ( x e. dom H |-> ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) ) >. e. _V
20 19 a1i 
 |-  ( ph -> <. ( ( 1st ` F ) |` dom dom H ) , ( x e. dom H |-> ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) ) >. e. _V )
21 4 16 17 18 20 ovmpod 
 |-  ( ph -> ( F |`f H ) = <. ( ( 1st ` F ) |` dom dom H ) , ( x e. dom H |-> ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) ) >. )