# Strictly Well-Founded Relation determines Strictly Minimal Elements/Lemma

This article needs to be linked to other articles.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{MissingLinks}}` from the code. |

## Theorem

Let $\RR$ be a strictly well-founded relation on $A$.

Then $A$ has a strictly minimal element under $\RR$.

## Proof

*This page is beyond the scope of ZFC, and should not be used in anything other than the theory in which it resides.*

*If you see any proofs that link to this page, please insert this template at the top.*

*If you believe that the contents of this page can be reworked to allow ZFC, then you can discuss it at the talk page.*

The general strategy of the proof is as follows:

We will recursively define a certain subset, $a$, of $A$.

We will use the fact that $\RR$ is a strictly well-founded relation to choose a strictly minimal element $m$ of $a$.

Then we will prove that $m$ is in fact a strictly minimal element of $A$.

For each $x \in A$, let $\map {\RR^{-1} } x$ denote the preimage under $\RR$ of $x$ in $A$.

For each class $C$, let $\map R C$ denote the set of elements of $C$ of minimal rank, and let $\map R \O = \O$.

That is:

For a given class $C$, let $\alpha_C$ be the smallest ordinal such that:

- $C \cap \map V {\alpha_C} \ne \O$

where $V$ is the von Neumann hierarchy.

Then let $\map R C$ denote the set $C \cap \map V {\alpha_C}$.

Let $F$ be a function defined recursively:

- $\map F 0 = \map R A$
- $\ds \map F {n + 1} = \bigcup_{y \mathop \in \map F n} \map R {\map {\RR^{-1} } y}$

This page has been identified as a candidate for refactoring of basic complexity.In particular: Extract this lemma into its own page.Until this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

### Lemma

$\map F n$ is a set for each $n \in \omega$.

### Proof

Proceed by induction:

$\map R A$ is a set, so $\map F 0$ is a set.

Suppose that $\map R {\map F n}$ is a set.

We know that for each $y \in \map F n$, $\map R {\map {\RR^{-1} } y}$ is a set, so by the Axiom of Unions, $\map F {n + 1}$ is a set.

$\Box$

Let $\ds a = \bigcup_{n \mathop \in \omega} \map F n$.

By the Axiom of Unions, $a$ is a set.

Since $\map F n \subseteq A$ for each $n \in \omega$, $a \subseteq A$.

By Non-Empty Class has Element of Least Rank, $\map F 0 \ne \O$, so $a \ne \O$.

Since $\RR$ is strictly well-founded, $a$ has a strictly minimal element $m$ under $\RR$.

Aiming for a contradiction, suppose that $m$ is not a strictly minimal element under $\RR$ of $A$.

Then, by Characterization of Minimal Element,

- $\map {\RR^{-1} } m \ne \O$

By Non-Empty Class has Element of Least Rank, $\map {\RR^{-1} } m$ has an element $w$ of least rank.

\(\ds \exists n \in \N: \, \) | \(\ds m\) | \(\in\) | \(\ds \map F n\) | Definition of $a$ | ||||||||||

\(\ds w\) | \(\in\) | \(\ds \map F {n + 1}\) | Definition of $F$ | |||||||||||

\(\ds w\) | \(\in\) | \(\ds a\) | Definition of $a$ |

Therefore, $a \mathop \cap \map {\RR^{-1} } m \ne \O$, contradicting the fact that $m$ is a strictly minimal element under $\RR$ in $a$.

Thus we conclude that $m$ is a strictly minimal element under $\RR$ of $A$.

$\blacksquare$

## Also see

- Well-Founded Proper Relational Structure Determines Minimal Elementsâ€Ž
- Proper Well-Ordering Determines Smallest Elements

These are weaker results that do not require the Axiom of Foundation.

## Sources

- 1971: Gaisi Takeuti and Wilson M. Zaring:
*Introduction to Axiomatic Set Theory*: $\S 9.21$