Order Isomorphism on Strictly Well-Founded Relation preserves Strictly Well-Founded Structure

From ProofWiki
Jump to navigation Jump to search


Let $A_1$ and $A_2$ be classes.

Let $\prec_1$ and $\prec_2$ be relations.

Let $\phi: \struct {A_1, \prec_1} \to \struct {A_2, \prec_2}$ be an order isomorphism.

Then $\struct {A_1, \prec_1}$ is a strictly well-founded structure if and only if $\struct {A_2, \prec_2}$ is also a strictly well-founded structure.


Take any nonempty subset $B \subseteq A_1$.

From Order Isomorphism Preserves Strictly Minimal Elements:

$x$ is a strictly minimal element of $B$ if and only if $\map \phi x$ is a strictly minimal element of $\phi \sqbrk B$.

By the definition of strictly well-founded relation, $\struct {A_1, \prec_1}$ is strictly well-founded if and only if $\struct {A_2, \prec_2}$ is strictly well-founded.