Nonlimit Ordinal Cofinal to One

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x$ be a nonlimit non-empty ordinal.

Let $\operatorname{cof}$ denote the cofinal relation.


Let $1$ denote the ordinal one.


Then:

$\operatorname{cof} \left({x, 1}\right)$


Proof

Since $1 = 0^+$, $1$ is not a limit ordinal.

Let $\le$ denote the subset relation.


It follows that $0 < 1$ by Ordinal is Less than Successor.

Moreover, $1 \le x$ follows by the fact that $0 < x$ and Successor of Element of Ordinal is Subset.

Thus we have $0 < 1 \le x$ and so by Condition for Cofinal Nonlimit Ordinals:

$\operatorname{cof} \left({x, 1}\right)$

$\blacksquare$


Sources