I am learning about classical set theory and how $\mathbb{N}$ can be constructed from sets satisfying ZFC in such a way that the Peano arithmetic axioms are satisfied.
Although the construction is clever, it seems to me to be quite convoluted (particularly the way $\mathbb{R}$ is then constructed from Dedekind cuts!) and then a bunch of effort is needed to show that the basic properties we want $\mathbb{N}$ are still satisfied.
Even then - we do not claim that $\mathbb{N}$ is actually the construction from ZFC but rather than ZFC allows us to construct something which satisfies the properties we want in $\mathbb{N}$ (e.g. "quasi-$\mathbb{N}$"). The $\mathbb{N}$ we know and love is still sort of undefined, and the most succinct definition, if one is needed, is arguably Peano arithmetic (at least, that any model satisfying Peano axioms has the same key properties as $\mathbb{N}$).
My question: what was gained, mathematically, by constructing a quasi-$\mathbb{N}$ from ZFC?
Suppose instead that mathematicians simply accepted that $\mathbb{N}$ was fundamental and axiomatic, and it has the properties we like, and that the Peano axioms provide sufficient definition (inarguably simpler than ZFC!). In both cases we are left with a set of axioms which are unproven.
So why bother constructing quasi-$\mathbb{N}$ from ZFC at all?
