A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$, 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, $\lvert B\rvert \le n$, and $\lvert B\rvert = n$ implies $B = n$. It is proved by induction on $n$.

Base case $n = 0$. Since $0 = \varnothing$, a subset $B \subseteq 0$ satisfies $B = \varnothing = 0$; so $B$ is finite with $\lvert B\rvert = 0 \le 0$, and $\lvert B\rvert = 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 $\lvert C\rvert \le n$, and $\lvert C\rvert = n$ implies $C = n$.

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

Case $n \notin B$. Here $B = B'$ is finite with $\lvert B\rvert = k \le n$, and $k \le n \le \sigma(n)$ gives $\lvert B\rvert \le \sigma(n)$; moreover $\lvert B\rvert = \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'$, which exists because $\lvert B'\rvert = 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 \notin k$. Then $h$ is injective, because $g$ is injective and takes its values in $B' \subseteq n$, so no value $g(i)$ equals $n$; and $h$ is surjective onto $B = B' \cup \{n\}$. Hence $B \approx \sigma(k)$, so $B$ is finite with $\lvert B\rvert = \sigma(k)$.

In the case $n \in B$ we therefore have $\lvert B\rvert = \sigma(k) \le \sigma(n)$, because $k \le n$; and if $\lvert B\rvert = \sigma(n)$ then $\sigma(k) = \sigma(n)$, so $k = n$, so $B' = 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 = \lvert A\rvert$. 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 $\lvert u[B]\rvert \le n$, hence $B$ is finite with $\lvert B\rvert = \lvert u[B]\rvert \le n = \lvert A\rvert$.

Clause 3. If $B = A$ then $\lvert B\rvert = \lvert A\rvert$. Conversely assume $\lvert B\rvert = \lvert A\rvert = n$. Then $\lvert u[B]\rvert = \lvert B\rvert = 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 $\lvert f[A]\rvert = \lvert A\rvert$ 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')$ gives $b = f(g(b)) = f(g(b')) = b'$. So $g$ is a bijection by step 8.1.

Composing $f \circ g = \mathrm{id}_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)$.