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	$$⊢\left(X\in V\wedge A:X⟶X\right)\to F\in \left(1\mathrm{-aryF}X\right)$$

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		ffvelcdm	$$⊢\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	$$⊢X\in V\to \left(F\in \left(1\mathrm{-aryF}X\right)\leftrightarrow F:X^{\left\{0\right\}}⟶X\right)$$
12	10 11	imbitrrid	$$⊢X\in V\to \left(A:X⟶X\to F\in \left(1\mathrm{-aryF}X\right)\right)$$
13	12	imp	$$⊢\left(X\in V\wedge A:X⟶X\right)\to F\in \left(1\mathrm{-aryF}X\right)$$