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