Theorem 1arymaptf

Description: The mapping of unary (endo)functions is a function into the set of endofunctions. (Contributed by AV, 18-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		1arymaptfv.h	|- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) )
2		fv1arycl	|- ( ( h e. ( 1 -aryF X ) /\ x e. X ) -> ( h ` { <. 0 , x >. } ) e. X )
3	2	adantll	|- ( ( ( X e. V /\ h e. ( 1 -aryF X ) ) /\ x e. X ) -> ( h ` { <. 0 , x >. } ) e. X )
4	3	fmpttd	|- ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) : X --> X )
5		simpl	|- ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> X e. V )
6	5 5	elmapd	|- ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> ( ( x e. X |-> ( h ` { <. 0 , x >. } ) ) e. ( X ^m X ) <-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) : X --> X ) )
7	4 6	mpbird	|- ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) e. ( X ^m X ) )
8	7 1	fmptd	|- ( X e. V -> H : ( 1 -aryF X ) --> ( X ^m X ) )