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	⊢ ( 𝜑 → Fun 𝐹 )
	resfvresima.s	⊢ ( 𝜑 → 𝑆 ⊆ dom 𝐹 )
	resfvresima.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion	resfvresima	⊢ ( 𝜑 → ( ( 𝐻 ↾ ( 𝐹 “ 𝑆 ) ) ‘ ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		resfvresima.f	⊢ ( 𝜑 → Fun 𝐹 )
2		resfvresima.s	⊢ ( 𝜑 → 𝑆 ⊆ dom 𝐹 )
3		resfvresima.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4	3	fvresd	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
5	4	fveq2d	⊢ ( 𝜑 → ( ( 𝐻 ↾ ( 𝐹 “ 𝑆 ) ) ‘ ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑋 ) ) = ( ( 𝐻 ↾ ( 𝐹 “ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
6	1 2	jca	⊢ ( 𝜑 → ( Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹 ) )
7		funfvima2	⊢ ( ( Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹 ) → ( 𝑋 ∈ 𝑆 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑆 ) ) )
8	6 3 7	sylc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑆 ) )
9	8	fvresd	⊢ ( 𝜑 → ( ( 𝐻 ↾ ( 𝐹 “ 𝑆 ) ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑋 ) ) )
10	5 9	eqtrd	⊢ ( 𝜑 → ( ( 𝐻 ↾ ( 𝐹 “ 𝑆 ) ) ‘ ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑋 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑋 ) ) )