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 e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) )
Assertion	2arymaptfv	|- ( F e. ( 2 -aryF X ) -> ( H ` F ) = ( x e. X , y e. X |-> ( F ` { <. 0 , x >. , <. 1 , y >. } ) ) )

Proof

Step	Hyp	Ref	Expression
1		2arymaptf.h	|- H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. 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 e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( F ` { <. 0 , x >. , <. 1 , y >. } ) ) )
4		eqid	|- ( 0 ..^ 2 ) = ( 0 ..^ 2 )
5	4	naryrcl	|- ( h e. ( 2 -aryF X ) -> ( 2 e. NN0 /\ X e. _V ) )
6		mpoexga	|- ( ( X e. _V /\ X e. _V ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. _V )
7	6	anidms	|- ( X e. _V -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. _V )
8	5 7	simpl2im	|- ( h e. ( 2 -aryF X ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. _V )
9	3 1 8	fvmpt3	|- ( F e. ( 2 -aryF X ) -> ( H ` F ) = ( x e. X , y e. X |-> ( F ` { <. 0 , x >. , <. 1 , y >. } ) ) )