Theorem mptfvmpt

Description: A function in maps-to notation as the value of another function in maps-to notation. (Contributed by AV, 20-Aug-2022)

	Ref	Expression
Hypotheses	mptfvmpt.y	$$⊢y=Y\to M=\left(x\in V⟼A\right)$$
	mptfvmpt.g	$$⊢G=\left(y\in W⟼M\right)$$
	mptfvmpt.v	$$⊢V=F\left(X\right)$$
Assertion	mptfvmpt	$$⊢Y\in W\to G\left(Y\right)=\left(x\in V⟼A\right)$$

Proof

Step	Hyp	Ref	Expression
1		mptfvmpt.y	$$⊢y=Y\to M=\left(x\in V⟼A\right)$$
2		mptfvmpt.g	$$⊢G=\left(y\in W⟼M\right)$$
3		mptfvmpt.v	$$⊢V=F\left(X\right)$$
4	3	fvexi	$$⊢V\in \mathrm{V}$$
5	4	mptex	$$⊢\left(x\in V⟼A\right)\in \mathrm{V}$$
6	1 2 5	fvmpt	$$⊢Y\in W\to G\left(Y\right)=\left(x\in V⟼A\right)$$