A subset of a finite set is finite, with $\mid B\mid \le \mid A\mid$, and equality holds if and only if $B=A$

The whole theorem rests on the special case where the ambient set is a natural number, which we call $(\ast )$: for every $n\in \mathbb{N}$ and every $B\subseteq n$, the set $B$ is finite, $\mid B\mid \le n$, and $\mid B\mid =n$ implies $B=n$. It is proved by induction on $n$.

Base case $n=0$. Since $0=\mathrm{\varnothing }$, a subset $B\subseteq 0$ satisfies $B=\mathrm{\varnothing }=0$; so $B$ is finite with $\mid B\mid =0\le 0$, and $\mid B\mid =0$ indeed gives $B=0$.

Inductive hypothesis. Fix $n\in \mathbb{N}$ and assume $(\ast )$ holds for $n$: every $C\subseteq n$ is finite with $\mid C\mid \le n$, and $\mid C\mid =n$ implies $C=n$.

Let $B\subseteq \sigma (n)=n\cup \{n\}$ and put $B^{\mathrm{\prime }}:=B\cap n$, so that $B^{\mathrm{\prime }}\subseteq n$, and $B=B^{\mathrm{\prime }}$ when $n\mathrm{\notin }B$ while $B=B^{\mathrm{\prime }}\cup \{n\}$ with $n\mathrm{\notin }{B}^{\mathrm{\prime }}$ when $n\in B$. By the inductive hypothesis of step 1.3 the set $B^{\mathrm{\prime }}$ is finite; write $k:=\mid B^{\mathrm{\prime }}\mid$, so $k\le n$, and $k=n$ forces $B^{\mathrm{\prime }}=n$.

Case $n\mathrm{\notin }B$. Here $B=B^{\mathrm{\prime }}$ is finite with $\mid B\mid =k\le n$, and $k\le n\le \sigma (n)$ gives $\mid B\mid \le \sigma (n)$; moreover $\mid B\mid =\sigma (n)$ is impossible, since $\sigma (n)=k\le n$ would give $n<n$ by [L6], so the third assertion of $(\ast )$ holds vacuously in this case.

Case $n\in B$. Choose a bijection $g:k\to B^{\mathrm{\prime }}$, which exists because $\mid B^{\mathrm{\prime }}\mid =k$, and define $h:\sigma (k)\to B$ by $h(i)=g(i)$ for $i\in k$ and $h(k)=n$; the two clauses do not conflict, since $k\mathrm{\notin }k$. Then $h$ is injective, because $g$ is injective and takes its values in $B^{\mathrm{\prime }}\subseteq n$, so no value $g(i)$ equals $n$; and $h$ is surjective onto $B=B^{\mathrm{\prime }}\cup \{n\}$. Hence $B\approx \sigma (k)$, so $B$ is finite with $\mid B\mid =\sigma (k)$.

In the case $n\in B$ we therefore have $\mid B\mid =\sigma (k)\le \sigma (n)$, because $k\le n$; and if $\mid B\mid =\sigma (n)$ then $\sigma (k)=\sigma (n)$, so $k=n$, so $B^{\mathrm{\prime }}=n$ and therefore $B=n\cup \{n\}=\sigma (n)$.

The two cases are exhaustive, so $(\ast )$ holds at $\sigma (n)$ whenever it holds at $n$; with the base case this gives $(\ast )$ for every $n\in \mathbb{N}$.

Clauses 1 and 2 in general. Fix a bijection $u:A\to n$, available since $n=\mid A\mid$. Then $u[B]\subseteq n$, and the restriction of $u$ to $B$ is a bijection of $B$ onto $u[B]$, so $B\approx u[B]$. By $(\ast )$ the set $u[B]$ is finite with $\mid u[B]\mid \le n$, hence $B$ is finite with $\mid B\mid =\mid u[B]\mid \le n=\mid A\mid$.

Clause 3. If $B=A$ then $\mid B\mid =\mid A\mid$. Conversely assume $\mid B\mid =\mid A\mid =n$. Then $\mid u[B]\mid =\mid B\mid =n$ by transport, so $u[B]=n$ by $(\ast )$, and therefore $B=u^{-1}[u[B]]=u^{-1}[n]=A$, because $u$ is a bijection of $A$ onto $n$.

Clause 4, the injective half. Let $f:A\to A$ be injective. Then $f$ is a bijection of $A$ onto its image $f[A]\subseteq A$, so $\mid f[A]\mid =\mid A\mid$ by transport, and clause 3 gives $f[A]=A$. Thus $f$ is surjective, hence a bijection.

Clause 4, the surjective half. Let $f:A\to A$ be surjective. For each $b\in A$ the set $u[f^{-1}[\{b\}]]\subseteq n$ is nonempty, so it has a least element by [L7]; let $g(b)$ be the value of $u^{-1}$ at that least element. No choice principle is used, since each $g(b)$ is determined by $b$ rather than selected. By construction $g(b)\in f^{-1}[\{b\}]$, that is $f(g(b))=b$ for every $b$; and $g$ is injective, since $g(b)=g(b^{\mathrm{\prime }})$ gives $b=f(g(b))=f(g(b^{\mathrm{\prime }}))=b^{\mathrm{\prime }}$. So $g$ is a bijection by step 8.1.

Composing $f\circ g={\mathrm{i}\mathrm{d}}_A$ on the right with $g^{-1}$ gives $f=g^{-1}$, which is a bijection; so a surjection of $A$ onto itself is a bijection, and in particular an injection.

Clauses 1 and 2 are step 6.1, clause 3 is step 7.1, and clause 4 is steps 8.1 and 10.1, each resting on the induction that establishes $(\ast )$.