This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑌 ∈ 𝑊 → ( 𝐺 ‘ 𝑌 ) = ( 𝑥 ∈ 𝑉 ↦ 𝐴 ) )