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	|- ( n e. NN |-> ( ! ` n ) ) e. ( NN ^m NN )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( n e. NN |-> ( ! ` n ) ) = ( n e. NN |-> ( ! ` n ) )
2		nnnn0	|- ( n e. NN -> n e. NN0 )
3	2	faccld	|- ( n e. NN -> ( ! ` n ) e. NN )
4	1 3	fmpti	|- ( n e. NN |-> ( ! ` n ) ) : NN --> NN
5		nnex	|- NN e. _V
6	5 5	elmap	|- ( ( n e. NN |-> ( ! ` n ) ) e. ( NN ^m NN ) <-> ( n e. NN |-> ( ! ` n ) ) : NN --> NN )
7	4 6	mpbir	|- ( n e. NN |-> ( ! ` n ) ) e. ( NN ^m NN )