Theorem 1arympt1

Description: A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024)

	Ref	Expression
Hypothesis	1arympt1.f	|- F = ( x e. ( X ^m { 0 } ) |-> ( A ` ( x ` 0 ) ) )
Assertion	1arympt1	|- ( ( X e. V /\ A : X --> X ) -> F e. ( 1 -aryF X ) )

Proof

Step	Hyp	Ref	Expression
1		1arympt1.f	|- F = ( x e. ( X ^m { 0 } ) |-> ( A ` ( x ` 0 ) ) )
2		eqid	|- ( X ^m { 0 } ) = ( X ^m { 0 } )
3		id	|- ( x e. ( X ^m { 0 } ) -> x e. ( X ^m { 0 } ) )
4		c0ex	|- 0 e. _V
5	4	snid	|- 0 e. { 0 }
6	5	a1i	|- ( x e. ( X ^m { 0 } ) -> 0 e. { 0 } )
7	2 3 6	mapfvd	|- ( x e. ( X ^m { 0 } ) -> ( x ` 0 ) e. X )
8		ffvelrn	|- ( ( A : X --> X /\ ( x ` 0 ) e. X ) -> ( A ` ( x ` 0 ) ) e. X )
9	7 8	sylan2	|- ( ( A : X --> X /\ x e. ( X ^m { 0 } ) ) -> ( A ` ( x ` 0 ) ) e. X )
10	9 1	fmptd	|- ( A : X --> X -> F : ( X ^m { 0 } ) --> X )
11		1aryfvalel	|- ( X e. V -> ( F e. ( 1 -aryF X ) <-> F : ( X ^m { 0 } ) --> X ) )
12	10 11	syl5ibr	|- ( X e. V -> ( A : X --> X -> F e. ( 1 -aryF X ) ) )
13	12	imp	|- ( ( X e. V /\ A : X --> X ) -> F e. ( 1 -aryF X ) )