Well-Founded Proper Relational Structure Determines Minimal Elements

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $A$ and $B$ be classes.

Let $\struct {A, \prec}$ be a proper relational structure.

Let $\prec$ be a strictly well-founded relation.


Suppose $B \subset A$ and $B \ne \O$.


Then $B$ has a strictly minimal element under $\prec$.


Proof

$B$ is not empty.

So $B$ has at least one element $x$.

By Singleton of Element is Subset:

$\set x \subseteq B$

By Relational Closure Exists for Set-Like Relation:

$\set x$ has a $\prec$-relational closure.



This $\prec$-relational closure shall be denoted $y$.

By Intersection is Subset:

$y \cap B \subseteq A$

As $x \in y$ and $x \in B$:

$y \cap B \ne \O$


By the definition of strictly well-founded relation:

$(1): \quad \exists x \in \paren {y \cap B}: \forall w \in \paren {y \cap B}: w \nprec x$


Aiming for a contradiction, suppose that $w \in B$ such that $w \prec x$.

Since $x \in y$, it follows that $w \in y$, so $w \in \paren {B \cap y}$ by the definition of intersection.

This contradicts $(1)$.

Therefore:

$w \nprec x$

and so $B$ has a strictly minimal element under $\prec$.

$\blacksquare$


Sources