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

Metamath Proof Explorer

Theorem resfvresima

Description: The value of the function value of a restriction for a function restricted to the image of the restricting subset. (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses resfvresima.f 
|- ( ph -> Fun F )
resfvresima.s 
|- ( ph -> S C_ dom F )
resfvresima.x 
|- ( ph -> X e. S )
Assertion resfvresima 
|- ( ph -> ( ( H |` ( F " S ) ) ` ( ( F |` S ) ` X ) ) = ( H ` ( F ` X ) ) )

Proof

Step Hyp Ref Expression
1 resfvresima.f 
 |-  ( ph -> Fun F )
2 resfvresima.s 
 |-  ( ph -> S C_ dom F )
3 resfvresima.x 
 |-  ( ph -> X e. S )
4 3 fvresd 
 |-  ( ph -> ( ( F |` S ) ` X ) = ( F ` X ) )
5 4 fveq2d 
 |-  ( ph -> ( ( H |` ( F " S ) ) ` ( ( F |` S ) ` X ) ) = ( ( H |` ( F " S ) ) ` ( F ` X ) ) )
6 1 2 jca 
 |-  ( ph -> ( Fun F /\ S C_ dom F ) )
7 funfvima2 
 |-  ( ( Fun F /\ S C_ dom F ) -> ( X e. S -> ( F ` X ) e. ( F " S ) ) )
8 6 3 7 sylc 
 |-  ( ph -> ( F ` X ) e. ( F " S ) )
9 8 fvresd 
 |-  ( ph -> ( ( H |` ( F " S ) ) ` ( F ` X ) ) = ( H ` ( F ` X ) ) )
10 5 9 eqtrd 
 |-  ( ph -> ( ( H |` ( F " S ) ) ` ( ( F |` S ) ` X ) ) = ( H ` ( F ` X ) ) )