Strictly Well-Founded Relation is Antireflexive

From ProofWiki
Jump to navigation Jump to search


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

Then $\RR$ is antireflexive.


Let $\struct {S, \preceq}$ be an ordered set.

Suppose that $S$ is non-empty.

Then $\preceq$ is not a strictly well-founded relation.


Let $p \in A$.

Then $\set p \ne \O$ and $\set p \subseteq A$.

Thus, by the definition of strictly well-founded relation:

$\exists x \in \set p: \forall y \in \set p: \neg \paren {y \mathrel \RR x}$

Since $x \in \set p$, it must be that $x = p$.

It follows that $p \not \mathrel \RR p$.

Since this holds for all $p \in A$, $\RR$ is antireflexive.