Technically, we should fix an ordinal and define by recursion on in the Well-ordered set .
By uniqueness in recursion, this gives a well-defined for all .
In general, this justifies recursive definition on all ordinals like the one above.
Similarly, proof by induction on all ordinals works:
Lemma
Let be some property of an ordinal .
Then
Proof
Assume otherwise.
Then there is an ordinal such that .
Then there is also a least ordinal such that .
If , then and so holds. By assumption holds.
Proposition
Proof
By induction on ( fixed).
Consider three cases:
If if then so .
If if then WLOG , and so .
So by induction
Finally, if is a limit. WLOG .
Then there is some such that .
By induction
Lemma
Let be a nonempty set of ordinals.
Then for any ordinal ,
Proof
Cases on whether has a greatest element.
Proposition
Proof
By induction on with , fixed. We consider three cases:
a limit