Theorem 1arymaptfv

Description: The value of the mapping of unary (endo)functions. (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	1arymaptfv	Could not format assertion : No typesetting found for |- ( F e. ( 1 -aryF X ) -> ( H ` F ) = ( x e. X |-> ( F ` { <. 0 , 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		fveq1	$$⊢h=F\to h\left(\left\{⟨0,x⟩\right\}\right)=F\left(\left\{⟨0,x⟩\right\}\right)$$
3	2	mpteq2dv	$$⊢h=F\to \left(x\in X⟼h\left(\left\{⟨0,x⟩\right\}\right)\right)=\left(x\in X⟼F\left(\left\{⟨0,x⟩\right\}\right)\right)$$
4		eqid	$$⊢\left(0..^1\right)=\left(0..^1\right)$$
5	4	naryrcl	Could not format ( h e. ( 1 -aryF X ) -> ( 1 e. NN0 /\ X e. _V ) ) : No typesetting found for |- ( h e. ( 1 -aryF X ) -> ( 1 e. NN0 /\ X e. _V ) ) with typecode |-
6	5	simprd	Could not format ( h e. ( 1 -aryF X ) -> X e. _V ) : No typesetting found for |- ( h e. ( 1 -aryF X ) -> X e. _V ) with typecode |-
7	6	mptexd	Could not format ( h e. ( 1 -aryF X ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) e. _V ) : No typesetting found for |- ( h e. ( 1 -aryF X ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) e. _V ) with typecode |-
8	3 1 7	fvmpt3	Could not format ( F e. ( 1 -aryF X ) -> ( H ` F ) = ( x e. X |-> ( F ` { <. 0 , x >. } ) ) ) : No typesetting found for |- ( F e. ( 1 -aryF X ) -> ( H ` F ) = ( x e. X |-> ( F ` { <. 0 , x >. } ) ) ) with typecode |-