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.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. 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$