Proof of Hartog's Theorem: Axiom of Replacement Applied

[mathshelp]

Write out the proof of Hartog's Theorem again carefully highlighting how the Axiom of Replacement is used

How can you highlight the axiom of replacment?

 

[JSuarez]

In the proof of Hartog's theorem, you reach a point where you just proved that the class of all well-orders of the set X (using the separation axiom schema). Now you have to prove that each the class of all order-types (isomorphic ordinals) of each of these well-orders is also a set, and it's here that you use replacement, by constructing a first-order formula that expresses the isomorphism of each (Y,<), where Y is a subset of X and "<" is a well-order in Y, to an ordinal.
This is the key step in Hartog's proof, the one that allows him to sidestep AC, so I think the "highlighting" is a careful, step-by-step explanation of how the replacement schema is used.

 

[mathshelp]

That makes sense, but how do you construct a first order formula?

 

[JSuarez]

I assume that, if you're studying formal Set Theory, that you are familiar with first-order logic (otherwise, it's impossible to understand anything of Set Theory).