Absoluteness of well-foundedness (source code)

= Absoluteness of well-foundedness

For a set relation in nested transitive models of <ZFC>, well-foundedness is absolute. An inner-model ordinal rank function witnesses upward absoluteness, and a fixed nonempty subset without a minimal member witnesses failure in both models.