Derived-set iteration of a well-order
ID: derived-set-iteration-of-a-well-order
For a well-ordered set , let contain the points whose strict initial segments are nonempty and have no greatest element, and iterate this operation transfinitely, taking intersections at limit stages. Every nonempty derivative loses at least its least element. If no derivative became empty, choosing one point from each successive difference would inject the ordinal supplied by Hartogs theorem for into , a contradiction.
New to topics? Read the docs here!