Proof of The Factorial as a Map on the Natural Numbers with Zero

Each result cited is universally quantified over the data in its own statement. It is applied to the data named where it is cited.

The inclusion map. For $k\in\mathbb{N}$ we have $k\in\mathbb{N}_{0}$, as $\mathbb{N}\subseteq\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, and $\mathbb{N}$ and $\mathbb{N}_{0}$ are sets by that clause. The expression $k$ contains no defined set symbol, so by Maps and Relations Given by Formulas §map there is a map $a:\mathbb{N}\to\mathbb{N}_{0}$ with $a(k)=k$ for every $k\in\mathbb{N}$; it is the map $k\mapsto k$ of Sets and Maps: Ordinary Notation §maps.

Partial products. By The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations and Multiplication on Omega: Products Lie in Omega, Multiplication Is a Binary Operation with Value the Product, and Membership in the Multiplication §operation, the multiplication $\cdot$ of $\mathbb{N}_{0}$ is a binary operation on the set $\mathbb{N}_{0}$, whose value at $(m,n)$ is the product $m\cdot n$, an element of $\mathbb{N}_{0}$ by Multiplication on Omega: Products Lie in Omega, Multiplication Is a Binary Operation with Value the Product, and Membership in the Multiplication §values. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §iterates, applied to $\cdot$, $X=\mathbb{N}_{0}$ and $a$, there is a map $s:\mathbb{N}\to\mathbb{N}_{0}$ with $s(n)=\prod_{k=1}^{n}a_{k}$ for every $n\in\mathbb{N}$; here $\prod_{k=1}^{n}a_{k}$ is the iterated operation of $a|_{[n]}$ by Iterated Operations: Finite Sums and Finite Products §restriction, written with $\prod$ by Iterated Operations: Finite Sums and Finite Products §sums.

The partial products are the factorials. Let $n\in\mathbb{N}$, and let $[n]$ be as in Intervals of Natural Numbers §segment. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[n]=\{k\in\mathbb{N}:k\le n\}\subseteq\mathbb{N}\subseteq\mathbb{N}_{0}$; it is a set by Sets and Maps: Ordinary Notation §set-builder. So, as for $a$, Maps and Relations Given by Formulas §map gives a map $b:[n]\to\mathbb{N}_{0}$ with $b(k)=k$ for every $k\in[n]$, the map $k\mapsto k$ on $[n]$ of Sets and Maps: Ordinary Notation §maps. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $a|_{[n]}$ is a function with domain $[n]\cap\operatorname{dom}a=[n]\cap\mathbb{N}=[n]$, using Functions, Values of a Function, and Functions from One Class to Another §map for $\operatorname{dom}a=\mathbb{N}$, and with value $a(k)=k$ at each $k\in[n]$. By Functions, Values of a Function, and Functions from One Class to Another §map, $b$ is a function with domain $[n]$, and its value at each $k\in[n]$ is $k$. Hence $a|_{[n]}=b$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, and $s(n)$ is the iterated operation of $b$, which is $\prod_{k=1}^{n}k$ in the notation of Iterated Operations: Finite Sums and Finite Products §iterated for the expression $k$. Now $1\le n$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order, and $\{1,\dots,n\}=[n]$ by Intervals of Natural Numbers §segment. By The Factorial of a Natural Number with Zero §factorial, $n!$ is the product $\prod_{k=1}^{n}k$ over the interval $\{1,\dots,n\}$, that is, of the map $b$ on $\{1,\dots,n\}$; as $\cdot$ is associative and commutative by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §associative and Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §commutative, Sums and Products over a Finite Set and over an Interval §intervals, with $m=1\le n$, shows that this product agrees with the iterated operation $\prod_{k=1}^{n}k$ of Iterated Operations: Finite Sums and Finite Products §iterated. Therefore $s(n)=n!$ for every $n\in\mathbb{N}$.

A formula by cases. The formulas below are formulas of class theory as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols, written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols and read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading. Elements of $\mathbb{N}_{0}$ are assigned to set variables and read as sets only in that sense; a variable to which a number is assigned occurs only to the left of $\in$, on either side of $=$, or as a component of an ordered pair. Assign $\mathbb{N}$ and $\mathbb{N}_{0}$ to distinct class variables $N$ and $M$, and $1$ and $s$ to distinct set variables $e$ and $s$, its parameters; let $w$ and $n$ be distinct set variables other than these. Let $\theta(w,n)$ be

$$(\neg\,n\in N\wedge w=e)\vee(n\in N\wedge(n,w)\in s),$$

and let $\gamma(n)$ be the atomic formula $n\in M$. The formula $\theta$ is written with the ordered pair, an abbreviation as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols, and applies no quantifier to a class variable, its parameters $N$, $e$ and $s$ occurring only free; so $\theta$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, and so is the atomic formula $\gamma$.

What the formula says. Let $n\in\mathbb{N}_{0}$ and let $w$ be a set. If $n\notin\mathbb{N}$, then $n=0$, as $\mathbb{N}=\mathbb{N}_{0}\setminus\{0\}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, and $\theta(w,n)$ holds if and only if $w=1$; and $1=0!$ by The Factorial: Recursion, Positivity and Bounds by Powers §recursion. If $n\in\mathbb{N}$, then $n\in\operatorname{dom}s$ by Functions, Values of a Function, and Functions from One Class to Another §map, and $\theta(w,n)$ holds if and only if $(n,w)\in s$, that is, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, if and only if $w=s(n)$, where $s(n)=n!$ by the preceding paragraphs. So for every set $n$ satisfying $\gamma(n)$, exactly one set $w$ satisfies $\theta(w,n)$, namely $n!$, which lies in $\mathbb{N}_{0}$ by The Factorial of a Natural Number with Zero §factorial.

Clause map. The formula $\theta$ is predicative, and by the preceding paragraph, for every set $n$ satisfying $\gamma(n)$ exactly one set $w$ satisfies $\theta(w,n)$. So Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols lets us introduce a defined set symbol $\tau(n)$, with argument the set $n$ and the parameters $N$, $e$ and $s$ of $\theta$ held fixed, as the unique set $w$ with $\theta(w,n)$; it is used properly wherever the hypothesis $n\in\mathbb{N}_{0}$ is in force, since that hypothesis ensures that exactly one such set exists. By the preceding paragraph, $\tau(n)=n!$ for every $n\in\mathbb{N}_{0}$. For $n\in\mathbb{N}_{0}$, the expression $\tau(n)\in\mathbb{N}_{0}$ stands, by the elimination rule of that clause, for $\exists z\,(\theta(z,n)\wedge z\in M)$, which by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination, with $k=1$, the formulas $\theta$ and $\gamma$ above and $\varphi(z,n)$ the atomic formula $z\in M$, holds if and only if the set $\tau(n)=n!$ lies in $\mathbb{N}_{0}$; it does, by the preceding paragraph. By Maps and Relations Given by Formulas §map, applied to the set $\mathbb{N}_{0}$ as domain and as codomain and to the expression $\tau(n)$, there is exactly one map $F:\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $F(n)=\tau(n)$ for every $n\in\mathbb{N}_{0}$. As $\tau(n)=n!$ for every $n\in\mathbb{N}_{0}$, the condition $F(n)=\tau(n)$ is the condition $F(n)=n!$, so exactly one map $F:\mathbb{N}_{0}\to\mathbb{N}_{0}$ has $F(n)=n!$ for every $n\in\mathbb{N}_{0}$; this is The Factorial as a Map on the Natural Numbers with Zero §map.

Clause values. Let $F$ be the map of The Factorial as a Map on the Natural Numbers with Zero §map. As $0\in\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, $F(0)=0!=1$ by The Factorial as a Map on the Natural Numbers with Zero §map and The Factorial: Recursion, Positivity and Bounds by Powers §recursion. Let $n\in\mathbb{N}_{0}$. Then $n+1\in\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations, so by The Factorial as a Map on the Natural Numbers with Zero §map, applied at $n+1$ and at $n$, and The Factorial: Recursion, Positivity and Bounds by Powers §recursion,

$$F(n+1)=(n+1)!=(n+1)\cdot n!=(n+1)\cdot F(n).$$