Theorem 1arymaptfv

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

	Ref	Expression
Hypothesis	1arymaptfv.h	|- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) )
Assertion	1arymaptfv	|- ( F e. ( 1 -aryF X ) -> ( H ` F ) = ( x e. X |-> ( F ` { <. 0 , x >. } ) ) )

Proof

Step	Hyp	Ref	Expression
1		1arymaptfv.h	|- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) )
2		fveq1	|- ( h = F -> ( h ` { <. 0 , x >. } ) = ( F ` { <. 0 , x >. } ) )
3	2	mpteq2dv	|- ( h = F -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) = ( x e. X |-> ( F ` { <. 0 , x >. } ) ) )
4		eqid	|- ( 0 ..^ 1 ) = ( 0 ..^ 1 )
5	4	naryrcl	|- ( h e. ( 1 -aryF X ) -> ( 1 e. NN0 /\ X e. _V ) )
6	5	simprd	|- ( h e. ( 1 -aryF X ) -> X e. _V )
7	6	mptexd	|- ( h e. ( 1 -aryF X ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) e. _V )
8	3 1 7	fvmpt3	|- ( F e. ( 1 -aryF X ) -> ( H ` F ) = ( x e. X |-> ( F ` { <. 0 , x >. } ) ) )