# Well-Founded Relation Determines Minimal Elements

## Contents

## Theorem

Let $A$ be a class.

Let $\prec$ be a foundational relation on $A$.

Let $B$ be a nonempty class such that $B \subseteq A$.

Then $B$ has a $\prec$-minimal element.

### Lemma

Let $\prec$ be a foundational relation on $A$.

Then $A$ has a $\prec$-minimal element.

## 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.*

Let $\prec' = \left({B \times B}\right) \cap {\prec}$.

by Restriction of Foundational Relation is Foundational, $\prec'$ is a foundational relation

By the lemma:

- $B$ has a $\prec'$-minimal element $m$.

By Minimal WRT Restriction, $m$ is $\prec$-minimal in $B$.

$\blacksquare$

## Also see

and

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$