
Ordinal Proof
Posted:
Jun 19, 2014 12:57 PM


Let S be a well ordered set. Recursively define an ordinal valued function f, over S by for all s in S, f(s) = { f(x)  x < a }
It's straight forward to show for all s, f(s) is hereditarily transitive, hence an ordinal; likewise eta + { f(x)  x in S } is an ordinal.
By construction f:S > eta is surjective. Additionally f is increasing for if a < b, then f(a) proper subset f(b), whence f(a) < f(b). Thusly f:S > eta is an order isomorphism.
eta is the unique ordinal order isomorphic to S for if pi is order isomorphic to S, then pi and eta are order isomorphic, hence equal.
Thus every well ordered set S, has a unique ordinal, the order type of S, that's order isomorphic to S.
I feel uneasy about that simple ZF proof, that it's flawed. Can I recursively construct a function into a class, ie a function with values that satisfy a proposition, but lacking a set for a codomain?
Hartog's lemma would provide such a set, but as it uses order types, it's not available to demonstrate a codomain set.
It there a patch for the proof?
A surer proof would be to show if every initial segment of S had an order type, then S would have an order type and forthwith show if some element of S didn't have an order type, then the least element of S without an order type, would have an order type. It however is three times as long.
Which proof would you prefer?

