Cardinality of Set is Finite iff Set is Finite
Jump to navigation
Jump to search
Theorem
Let $A$ be a set.
- $\card A$ is finite
- $A$ is finite
where $\card A$ denotes the cardinality of $A$.
Proof
Definition of cardinal:
- $(1): \quad \card A \sim A$
- $\card A$ is finite
- $\exists n \in \N: \card A \sim \N_n$ by definition of finite set
- $\exists n \in \N: A \sim \N_n$ by $(1)$ and Set Equivalence behaves like Equivalence Relation
- $A$ is finite by definition of finite set.
$\blacksquare$
Sources
- Mizar article CARD_1:funcreg 8