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	$⊢ φ \to Fun F$
		resfvresima.s	$⊢ φ \to S \subseteq dom F$
		resfvresima.x	$⊢ φ \to X \in S$
	Assertion	resfvresima	$⊢ φ \to ({H ↾}_{F [S]}) (({F ↾}_{S}) (X)) = H (F (X))$

Proof

Step	Hyp	Ref	Expression
1		resfvresima.f	$⊢ φ \to Fun F$
2		resfvresima.s	$⊢ φ \to S \subseteq dom F$
3		resfvresima.x	$⊢ φ \to X \in S$
4	3	fvresd	$⊢ φ \to ({F ↾}_{S}) (X) = F (X)$
5	4	fveq2d	$⊢ φ \to ({H ↾}_{F [S]}) (({F ↾}_{S}) (X)) = ({H ↾}_{F [S]}) (F (X))$
6	1 2	jca	$⊢ φ \to (Fun F \land S \subseteq dom F)$
7		funfvima2	$⊢ (Fun F \land S \subseteq dom F) \to (X \in S \to F (X) \in F [S])$
8	6 3 7	sylc	$⊢ φ \to F (X) \in F [S]$
9	8	fvresd	$⊢ φ \to ({H ↾}_{F [S]}) (F (X)) = H (F (X))$
10	5 9	eqtrd	$⊢ φ \to ({H ↾}_{F [S]}) (({F ↾}_{S}) (X)) = H (F (X))$