# Non-Empty Class has Element of Least Rank

This article needs proofreading.Please check it for mathematical errors.If you believe there are none, please remove `{{Proofread}}` from the code.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 `{{Proofread}}` from the code. |

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 $C$ be a class.

Let $C \ne \O$.

Then $C$ has an element of least rank.

That is:

- $\exists x \in C: \forall y \in C: \map {\operatorname {rank} } x \le \map {\operatorname {rank} } y$

where $\map {\operatorname {rank} } x$ 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.

This article, or a section of it, needs explaining.In particular: This should follow from arbitrary intersections of ordinals being ordinals.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.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 `{{Explain}}` from the code. |

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: \map {\operatorname {rank} } x = q$

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

$\blacksquare$