# Non-Empty Class has Element of Least Rank

## Theorem

Let $C$ be a class.

Let $C \ne \varnothing$.

Then $C$ has an element of least rank.

That is:

- $\exists x \in C: \forall y \in C: \operatorname{rank} \left({x}\right) \le \operatorname {rank}\left({y}\right)$

where $\operatorname{rank}\left({x}\right)$ is the rank of $x$.

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

By Set has Rank, each element of $C$ has a rank.

Let $R$ be the class of ranks of elements of $C$.

$R$ is non-empty because $C$ is non-empty.

Since any non-empty class of ordinals has a least element, $R$ has a least element, $q$.

By the definition of $R$:

- $\exists x \in C: \operatorname{rank}\left({x}\right) = q$

Then $x$ is an element of $C$ of least rank.

$\blacksquare$