Proof of The Natural Numbers Are Not Finite

Each result cited is universally quantified over the data in its own statement, and is applied here to the data named in the statement of this lemma.

Claim 1 (Clause 1). Suppose, for a contradiction, that $\mathbb{N}$ is finite. It is nonempty, since $1\in\mathbb{N}$. The successor map $S:\mathbb{N}\to\mathbb{N}$ is injective, this being one of the requirements imposed on the natural numbers in Natural Numbers. By claim 2 of An Injective Self-Map of a Finite Set is a Bijection, applied to the nonempty finite set $\mathbb{N}$ and to $S$, the map $S$ is a bijection from $\mathbb{N}$ onto $\mathbb{N}$. Applying Bijection of Sets to the element $1$ of the codomain, there is $j\in\mathbb{N}$ with $S(j)=1$. This contradicts the requirement $S(j)\ne1$, also imposed in Natural Numbers. Hence $\mathbb{N}$ is not finite.

Claim 2 (Clause 2). Let $X$ and $h$ be as in clause 2 and suppose, for a contradiction, that $X$ is finite. Put

By claim 3 of Basic Properties of Finite Sets, applied to the finite set $X$ and the subset $Y$, the set $Y$ is finite; and $Y$ is nonempty, since $h(1)\in Y$. By Finite Set a nonempty finite set has $p$ elements for some $p\in\mathbb{N}$; fix such a $p$ for $Y$. By Number of Elements of a Set there is then a bijection $f:[p]\to Y$, where $[p]$ is the initial segment determined by $p$.

Let $g:\mathbb{N}\to Y$ be the map with $g(m)=h(m)$, which is well defined by the definition of $Y$. It is a bijection: every $y\in Y$ equals $h(m)=g(m)$ for some $m\in\mathbb{N}$, by the definition of $Y$, and such an $m$ is unique because $h$ is injective; this is precisely the condition of Bijection of Sets.

By claim 2 of Inverse of a Bijection, applied to $f$, the map $f^{-1}:Y\to[p]$ is a bijection. By claim 2 of Injectivity, Composition, and Restriction of Bijections, applied to $g$ and to $f^{-1}$, the map $m\mapsto f^{-1}(g(m))$ is a bijection from $\mathbb{N}$ onto $[p]$; by claim 2 of Inverse of a Bijection, applied to that map, its inverse is a bijection from $[p]$ onto $\mathbb{N}$. Hence $\mathbb{N}$ has $p$ elements by Number of Elements of a Set, and so is finite by Finite Set, contradicting claim 1. Therefore $X$ is not finite.