Metamath Proof Explorer


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 n !

Proof

Step Hyp Ref Expression
1 eqid n n ! = n n !
2 nnnn0 n n 0
3 2 faccld n n !
4 1 3 fmpti n n ! :
5 nnex V
6 5 5 elmap n n ! n n ! :
7 4 6 mpbir n n !