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	No typesetting found for |- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) ) with typecode |-
Assertion	1arymaptf	Could not format assertion : No typesetting found for |- ( X e. V -> H : ( 1 -aryF X ) --> ( X ^m X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1arymaptfv.h	Could not format H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) ) : No typesetting found for |- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) ) with typecode |-
2		fv1arycl	Could not format ( ( h e. ( 1 -aryF X ) /\ x e. X ) -> ( h ` { <. 0 , x >. } ) e. X ) : No typesetting found for |- ( ( h e. ( 1 -aryF X ) /\ x e. X ) -> ( h ` { <. 0 , x >. } ) e. X ) with typecode |-
3	2	adantll	Could not format ( ( ( X e. V /\ h e. ( 1 -aryF X ) ) /\ x e. X ) -> ( h ` { <. 0 , x >. } ) e. X ) : No typesetting found for |- ( ( ( X e. V /\ h e. ( 1 -aryF X ) ) /\ x e. X ) -> ( h ` { <. 0 , x >. } ) e. X ) with typecode |-
4	3	fmpttd	Could not format ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) : X --> X ) : No typesetting found for |- ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) : X --> X ) with typecode |-
5		simpl	Could not format ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> X e. V ) : No typesetting found for |- ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> X e. V ) with typecode |-
6	5 5	elmapd	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
7	4 6	mpbird	Could not format ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) e. ( X ^m X ) ) : No typesetting found for |- ( ( X e. V /\ h e. ( 1 -aryF X ) ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) e. ( X ^m X ) ) with typecode |-
8	7 1	fmptd	Could not format ( X e. V -> H : ( 1 -aryF X ) --> ( X ^m X ) ) : No typesetting found for |- ( X e. V -> H : ( 1 -aryF X ) --> ( X ^m X ) ) with typecode |-