Theorem 1arympt1

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

	Ref	Expression
Hypothesis	1arympt1.f	$$⊢F=\left(x\in \left(X^{\left\{0\right\}}\right)⟼A\left(x\left(0\right)\right)\right)$$
Assertion	1arympt1	Could not format assertion : No typesetting found for |- ( ( X e. V /\ A : X --> X ) -> F e. ( 1 -aryF X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1arympt1.f	$$⊢F=\left(x\in \left(X^{\left\{0\right\}}\right)⟼A\left(x\left(0\right)\right)\right)$$
2		eqid	$$⊢X^{\left\{0\right\}}=X^{\left\{0\right\}}$$
3		id	$$⊢x\in \left(X^{\left\{0\right\}}\right)\to x\in \left(X^{\left\{0\right\}}\right)$$
4		c0ex	$$⊢0\in \mathrm{V}$$
5	4	snid	$$⊢0\in \left\{0\right\}$$
6	5	a1i	$$⊢x\in \left(X^{\left\{0\right\}}\right)\to 0\in \left\{0\right\}$$
7	2 3 6	mapfvd	$$⊢x\in \left(X^{\left\{0\right\}}\right)\to x\left(0\right)\in X$$
8		ffvelrn	$$⊢\left(A:X⟶X\wedge x\left(0\right)\in X\right)\to A\left(x\left(0\right)\right)\in X$$
9	7 8	sylan2	$$⊢\left(A:X⟶X\wedge x\in \left(X^{\left\{0\right\}}\right)\right)\to A\left(x\left(0\right)\right)\in X$$
10	9 1	fmptd	$$⊢A:X⟶X\to F:X^{\left\{0\right\}}⟶X$$
11		1aryfvalel	Could not format ( X e. V -> ( F e. ( 1 -aryF X ) <-> F : ( X ^m { 0 } ) --> X ) ) : No typesetting found for |- ( X e. V -> ( F e. ( 1 -aryF X ) <-> F : ( X ^m { 0 } ) --> X ) ) with typecode |-
12	10 11	syl5ibr	Could not format ( X e. V -> ( A : X --> X -> F e. ( 1 -aryF X ) ) ) : No typesetting found for |- ( X e. V -> ( A : X --> X -> F e. ( 1 -aryF X ) ) ) with typecode |-
13	12	imp	Could not format ( ( X e. V /\ A : X --> X ) -> F e. ( 1 -aryF X ) ) : No typesetting found for |- ( ( X e. V /\ A : X --> X ) -> F e. ( 1 -aryF X ) ) with typecode |-