Cardinality

DEF-CARD. Cardinality. $\limp\AC$

If we assume $\AC$, then every set $X$ can be well-ordered (PROP-WOT). By PROP-OT, there is at least one ordinal that is equinumerous to $X$. We define the cardinality of $X$ as the least such ordinal:

\[\lvert X\rvert = \min\{\alpha\in\Ord:X\equ\alpha\}.\]

PROP-CARD.

For any $X$ and $Y$:

1. \[X\equ Y \enspace\lrimp\enspace \lvert X\rvert=\lvert Y\rvert.\]
2. \[X\lequ Y \enspace\lrimp\enspace \lvert X\rvert\leq\lvert Y\rvert.\]
3. \[X\lnequ Y \enspace\lrimp\enspace \lvert X\rvert<\lvert Y\rvert.\]