Restriction of Well-Founded Ordering
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
To discuss this in more detail, feel free to use the talk page.
Once you have done so, you can remove this instance of {{MissingLinks}} from the code.
Theorem
Let $T$ be a subset or subclass of $S$.
Let $\preceq$ be a well-founded ordering of $A$.
Let $\preceq'$ be the restriction of $\preceq$ to $T$.
Then $\preceq'$ is a well-founded ordering of $T$.
Proof
By Restriction of Ordering is Ordering, $\preceq'$ is an ordering.
Let $A$ be a non-empty subset of $T$.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
Then $A$ is a non-empty subset of $S$.
Since $\preceq$ is well-founded, $A$ has a minimal element $m$ with respect to $\preceq$.
Let $x \in A$ and suppose $x \preceq' m$.
Then by the definition of restriction, $x \preceq m$.
Thus by the definition of a minimal element, $x = m$.
As this holds for all $x \in A$, $m$ is minimal in $A$ with respect to $\preceq'$.
As this holds for all subsets $A$ of $T$, $\preceq'$ is a well-founded ordering of $T$.
$\blacksquare$
