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	⊢ ( 𝑦 = 𝑌 → 𝑀 = ( 𝑥 ∈ 𝑉 ↦ 𝐴 ) )
	mptfvmpt.g	⊢ 𝐺 = ( 𝑦 ∈ 𝑊 ↦ 𝑀 )
	mptfvmpt.v	⊢ 𝑉 = ( 𝐹 ‘ 𝑋 )
Assertion	mptfvmpt	⊢ ( 𝑌 ∈ 𝑊 → ( 𝐺 ‘ 𝑌 ) = ( 𝑥 ∈ 𝑉 ↦ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		mptfvmpt.y	⊢ ( 𝑦 = 𝑌 → 𝑀 = ( 𝑥 ∈ 𝑉 ↦ 𝐴 ) )
2		mptfvmpt.g	⊢ 𝐺 = ( 𝑦 ∈ 𝑊 ↦ 𝑀 )
3		mptfvmpt.v	⊢ 𝑉 = ( 𝐹 ‘ 𝑋 )
4	3	fvexi	⊢ 𝑉 ∈ V
5	4	mptex	⊢ ( 𝑥 ∈ 𝑉 ↦ 𝐴 ) ∈ V
6	1 2 5	fvmpt	⊢ ( 𝑌 ∈ 𝑊 → ( 𝐺 ‘ 𝑌 ) = ( 𝑥 ∈ 𝑉 ↦ 𝐴 ) )