Theorem facmapnn

Description: The factorial function restricted to positive integers is a mapping from the positive integers to the positive integers. (Contributed by AV, 8-Aug-2020)

	Ref	Expression
Assertion	facmapnn	$$⊢\left(n\in \mathbb{N}⟼n!\right)\in \left({\mathbb{N}}^{\mathbb{N}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(n\in \mathbb{N}⟼n!\right)=\left(n\in \mathbb{N}⟼n!\right)$$
2		nnnn0	$$⊢n\in \mathbb{N}\to n\in {\mathbb{N}}_0$$
3	2	faccld	$$⊢n\in \mathbb{N}\to n!\in \mathbb{N}$$
4	1 3	fmpti	$$⊢\left(n\in \mathbb{N}⟼n!\right):\mathbb{N}⟶\mathbb{N}$$
5		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
6	5 5	elmap	$$⊢\left(n\in \mathbb{N}⟼n!\right)\in \left({\mathbb{N}}^{\mathbb{N}}\right)\leftrightarrow \left(n\in \mathbb{N}⟼n!\right):\mathbb{N}⟶\mathbb{N}$$
7	4 6	mpbir	$$⊢\left(n\in \mathbb{N}⟼n!\right)\in \left({\mathbb{N}}^{\mathbb{N}}\right)$$