Metamath Proof Explorer


Theorem 2arymaptfv

Description: The value of the mapping of binary (endo)functions. (Contributed by AV, 21-May-2024)

Ref Expression
Hypothesis 2arymaptf.h 𝐻 = ( ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥𝑋 , 𝑦𝑋 ↦ ( ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
Assertion 2arymaptfv ( 𝐹 ∈ ( 2 -aryF 𝑋 ) → ( 𝐻𝐹 ) = ( 𝑥𝑋 , 𝑦𝑋 ↦ ( 𝐹 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )

Proof

Step Hyp Ref Expression
1 2arymaptf.h 𝐻 = ( ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥𝑋 , 𝑦𝑋 ↦ ( ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
2 fveq1 ( = 𝐹 → ( ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝐹 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) )
3 2 mpoeq3dv ( = 𝐹 → ( 𝑥𝑋 , 𝑦𝑋 ↦ ( ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) = ( 𝑥𝑋 , 𝑦𝑋 ↦ ( 𝐹 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
4 eqid ( 0 ..^ 2 ) = ( 0 ..^ 2 )
5 4 naryrcl ( ∈ ( 2 -aryF 𝑋 ) → ( 2 ∈ ℕ0𝑋 ∈ V ) )
6 mpoexga ( ( 𝑋 ∈ V ∧ 𝑋 ∈ V ) → ( 𝑥𝑋 , 𝑦𝑋 ↦ ( ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ∈ V )
7 6 anidms ( 𝑋 ∈ V → ( 𝑥𝑋 , 𝑦𝑋 ↦ ( ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ∈ V )
8 5 7 simpl2im ( ∈ ( 2 -aryF 𝑋 ) → ( 𝑥𝑋 , 𝑦𝑋 ↦ ( ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ∈ V )
9 3 1 8 fvmpt3 ( 𝐹 ∈ ( 2 -aryF 𝑋 ) → ( 𝐻𝐹 ) = ( 𝑥𝑋 , 𝑦𝑋 ↦ ( 𝐹 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )