Induction over all ordinal numbers. I'm starting to learn set theory. I've already learned transfinite induction and I started to wonder if we could do the same on a well-ordered proper class, like the class of all ordinal numbers. It seems intuitive to me that we should be able to prove statements about all ordinal numbers by induction. But I'm not sure what theory I need to do this. I don't know anything about set theories other than ZFC, and I still don't really know much about ZFC, so I'm not sure what is and what isn't allowed in ZFC regarding proper classes. For example, I don't know if it's possible to say in ZFC that the class of all ordinal numbers exists. I think it might not be possible. But then maybe I don't need to talk about this class to perform induction over it. Maybe I just need to know what an ordinal number is, and this I know to be sayable.
Could you help me understand this? Please, if there is the slightest chance I won't understand a term or a notion, assume that I won't. I'm new to set theory.
 A: ZF(C) doesn’t have proper classes, but as you say, it is possible to write down a predicate $\varphi(x)$ that ‘says’ that $x$ is an ordinal. We can then write $x\in\mathbf{ON}$ with the understanding that it really means $\varphi(x)$. Similarly, if $\varphi(x,y)$ is some two-place predicate, we might be able to prove $$\forall x,y,z\big(\varphi(x,y)\land\varphi(x,z)\to y=z\big)\;,$$ in which case we could write $y=\mathbf{F}(x)$ as an abbreviation for $\varphi(x,y)$ and think of $\mathbf{F}$ as a function, albeit one that might be a proper class (if ZF(C) actually had such things formally).
Yes, it’s possible to do transfinite induction over all ordinals. It’s even possible to do recursive constructions over all ordinals. The theorems, which already hold in ZF, can be stated as follows, where boldface indicates ‘proper classes’ of the definable sort that I described above:

Theorem (Transfinite Induction): If $\varnothing\ne\mathbf{C}\subseteq\mathbf{ON}$, then $\mathbf{C}$ has a least element.
Theorem (Transfinite Recursion): If $\mathbf{F}:\mathbf{V}\to\mathbf{V}$, then there is a unique $\mathbf{G}:\mathbf{ON}\to\mathbf{V}$ such that $\forall\alpha\big(\mathbf{G}(\alpha)=\mathbf{F}(\mathbf{G}\upharpoonright\alpha)\big)$.

(These formulations are essentially the ones used in K. Kunen’s Set Theory.)
