Sorry, I don't have enough reputation to post a picture, so here's a link:
https://i.stack.imgur.com/XxYif.png
The above theorem is proved using transfinite induction, but this relies on there being a first order predicate expressing "this ordinal may be expressed in the cantor normal form" for this to follow from the axioms of ZFC. I am looking for a brief sketch of how one could go about doing this.
I think part of what has me stumped is the fact that n can vary so I can't simply just put a fixed number of existential quantifiers in my first order formula.