Well-ordered sets are order-isomorphic to a unique ordinal and proof by induction over the ordinals I've read through the various threads concerning the proof that every well-ordered set is order isomorphic to an ordinal, and I have a thousand questions. Let me concentrate on one.  I'm reading a set theory book by Judith Roitman called Introduction to Modern Set Theory, and my question is not so much about the result itself, but about her proof by transfinite induction, and how it relates to proofs in general that use transfinite induction. 
Let me start with Roitman's proof. Let $x$ be a well-ordered set. We will define a function by induction whose range is $x$ and whose domain is an ordinal $\alpha$. The proof is by induction over $\alpha$. Let $f(0)$ be the minimum of $x$, which exists since $x$ is well-ordered [defining $f(0)$ can be and should be neglected since $x=\varnothing$ is a possibility, as per the discussion below]. Assume we have defined $f(\beta)$ for $\beta < \alpha$, where $\alpha$ is some ordinal. That is to say, we have defined $f: \alpha \to x$ for all $\beta \in \alpha$, i.e. for all $\beta < \alpha$. We need to define $f(\alpha)$. Let $f[\alpha]$ be the image of $\alpha$ under $f$, i.e. $f[\alpha] = \{f(\beta) \vert \beta < \alpha \}$. If $f[\alpha] \ne x$ then define $f(\alpha)$ as the minimum of $x \setminus f[\alpha] \ne \varnothing$. If $f[\alpha]=x$ then we are finished, and we have defined $f:\alpha \to x$. How do we know that we can finish in this manner? What if it keeps going and $f[\alpha]$ is never equal to $x$? I think this same question holds for almost every other proof by transfinite induction. 
This proof looks nothing like the others in this thread. Is this a correct use of transfinite induction? How do we know that eventually $f[\alpha]=x$ for some $\alpha$? There was an interesting thread about the axiom of replacement being crucial to this theorem. If the above proof is correct, then replacement must be implicit. But where? Thanks for any insights you can provide. 
 A: This indeed requires more justification.  The key point is that $f$ is injective, so $f^{-1}$ is a well-defined function on the image of $f$.  If there does not exist any $\alpha$ such that $f[\alpha]=x$, then $f$ is defined on the entire class $Ord$ of ordinals, and so $f^{-1}$ is surjection $A\to Ord$ where $A$ is the image of $f$ (a set by Separation, since it is a subset of $x$).  But then by Replacement the image $f^{-1}[A]=Ord$ is a set, which is a contradiction (by the Burali-Forti paradox).
By the way, it is possible to avoid Replacement in justifying many arguments of this sort.  For any set $X$, you can prove (without Replacement or Choice) that there exists a well-ordered set $W$ such that there exists no injection $W\to X$, and then use transfinite recursion on $W$ instead of on $Ord$.  See this answer of mine for more details.  This doesn't work for a statement like the one you mention where the conclusion itself involves ordinals, but it works for many other proofs whose conclusions aren't about ordinals (e.g., things like "every vector space has a basis", where you construct a basis by building it one element at a time by transfinite recursion).
