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 ⊢ H = h ∈ 2 -aryF X ⟼ x ∈ X , y ∈ X ⟼ h ⁡ 0 x 1 y
Assertion 2arymaptfv ⊢ F ∈ 2 -aryF X → H ⁡ F = x ∈ X , y ∈ X ⟼ F ⁡ 0 x 1 y

Proof

Step Hyp Ref Expression
1 2arymaptf.h ⊢ H = h ∈ 2 -aryF X ⟼ x ∈ X , y ∈ X ⟼ h ⁡ 0 x 1 y
2 fveq1 ⊢ h = F → h ⁡ 0 x 1 y = F ⁡ 0 x 1 y
3 2 mpoeq3dv ⊢ h = F → x ∈ X , y ∈ X ⟼ h ⁡ 0 x 1 y = x ∈ X , y ∈ X ⟼ F ⁡ 0 x 1 y
4 eqid ⊢ 0 ..^ 2 = 0 ..^ 2
5 4 naryrcl ⊢ h ∈ 2 -aryF X → 2 ∈ ℕ 0 ∧ X ∈ V
6 mpoexga ⊢ X ∈ V ∧ X ∈ V → x ∈ X , y ∈ X ⟼ h ⁡ 0 x 1 y ∈ V
7 6 anidms ⊢ X ∈ V → x ∈ X , y ∈ X ⟼ h ⁡ 0 x 1 y ∈ V
8 5 7 simpl2im ⊢ h ∈ 2 -aryF X → x ∈ X , y ∈ X ⟼ h ⁡ 0 x 1 y ∈ V
9 3 1 8 fvmpt3 ⊢ F ∈ 2 -aryF X → H ⁡ F = x ∈ X , y ∈ X ⟼ F ⁡ 0 x 1 y