Transfinite induction

Let $(W, <)$ be a well-order (Well-order and well-ordered set) and let $S \subseteq W$ satisfy the following: for every $a \in W$, if $W_{<a} \subseteq S$ then $a \in S$ (Initial segment of a well-order). Then $S = W$.

In property form: if a property $P$ of elements of $W$ satisfies "whenever $P(x)$ holds for every $x < a$, it holds at $a$", then $P(a)$ holds for every $a \in W$.

This is a theorem of ZF. No form of the Axiom of Choice is used. Choice is perfectly available at this point in the library, since Zorn's lemma is proved from it on the previous page; the claim made here is about this proof, which never invokes it.

Where the well-ordering is used. Only once, to produce the least element of $W \setminus S$. Nothing else about $W$ enters the argument, so the same proof establishes the statement for an arbitrary well-founded relation once that notion is available.

No separate base case. Applying the hypothesis at $a = \min W$, when $W$ is nonempty, forces $\min W \in S$, because the initial segment below $\min W$ is empty and is therefore contained in $S$ vacuously. This is why transfinite induction is stated with a single clause where ordinary induction has two, and it is also why the statement holds vacuously for $W = \emptyset$.

Successors and limits. The scheme that looks stronger, with one clause for the least element, one for successors and one for limits, is the specialisation of this theorem to a well-order in which those three kinds of element are distinguished. Nothing is gained by assuming it separately, and the three-clause form is what gets used once ordinals are available.

Least counterexample. The dual reading is often the useful one: if $S \ne W$ then the hypothesis must fail somewhere, so there is a least $a$ with $a \notin S$ and every $x < a$ in $S$. Steps 2.1 to 5.1 are precisely the construction of that least counterexample.