Set of Cardinality not Greater than Cardinality of Finite Set is Finite
Jump to navigation
Jump to search
Theorem
Let $X, Y$ be sets such that
- $\card X \le \card Y$
and
- $Y$ is finite,
where $\card X$ denotes the cardinality of $X$.
Then $X$ is finite.
Proof
By Finite iff Cardinality Less than Aleph Zero:
- $\card Y < \aleph_0$
Then
- $\card X < \aleph_0$
Thus by Finite iff Cardinality Less than Aleph Zero:
- $X$ is a finite set.
$\blacksquare$
Sources
- Mizar article CARD_2:49