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	⊢ ( 𝑛 ∈ ℕ ↦ ( ! ‘ 𝑛 ) ) ∈ ( ℕ ↑m ℕ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( ! ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ! ‘ 𝑛 ) )
2		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
3	2	faccld	⊢ ( 𝑛 ∈ ℕ → ( ! ‘ 𝑛 ) ∈ ℕ )
4	1 3	fmpti	⊢ ( 𝑛 ∈ ℕ ↦ ( ! ‘ 𝑛 ) ) : ℕ ⟶ ℕ
5		nnex	⊢ ℕ ∈ V
6	5 5	elmap	⊢ ( ( 𝑛 ∈ ℕ ↦ ( ! ‘ 𝑛 ) ) ∈ ( ℕ ↑m ℕ ) ↔ ( 𝑛 ∈ ℕ ↦ ( ! ‘ 𝑛 ) ) : ℕ ⟶ ℕ )
7	4 6	mpbir	⊢ ( 𝑛 ∈ ℕ ↦ ( ! ‘ 𝑛 ) ) ∈ ( ℕ ↑m ℕ )