Theorem 1arymaptf1o

Description: The mapping of unary (endo)functions is a one-to-one function onto the set of endofunctions. (Contributed by AV, 19-May-2024)

	Ref	Expression
Hypothesis	1arymaptfv.h	$$⊢H=\left(h\in \left(1\mathrm{-aryF}X\right)⟼\left(x\in X⟼h\left(\left\{⟨0,x⟩\right\}\right)\right)\right)$$
Assertion	1arymaptf1o	$$⊢X\in V\to H:1\mathrm{-aryF}X\underset{1-1\; onto}{⟶}{X}^X$$

Proof

Step	Hyp	Ref	Expression
1		1arymaptfv.h	$$⊢H=\left(h\in \left(1\mathrm{-aryF}X\right)⟼\left(x\in X⟼h\left(\left\{⟨0,x⟩\right\}\right)\right)\right)$$
2	1	1arymaptf1	$$⊢X\in V\to H:1\mathrm{-aryF}X\underset{1-1}{⟶}{X}^X$$
3	1	1arymaptfo	$$⊢X\in V\to H:1\mathrm{-aryF}X\underset{onto}{⟶}{X}^X$$
4		df-f1o	$$⊢H:1\mathrm{-aryF}X\underset{1-1\; onto}{⟶}{X}^X\leftrightarrow \left(H:1\mathrm{-aryF}X\underset{1-1}{⟶}{X}^X\wedge H:1\mathrm{-aryF}X\underset{onto}{⟶}{X}^X\right)$$
5	2 3 4	sylanbrc	$$⊢X\in V\to H:1\mathrm{-aryF}X\underset{1-1\; onto}{⟶}{X}^X$$