Cardinality of Set is Finite iff Set is Finite

Theorem

Let $A$ be a set.

$\card A$ is finite

if and only if:

$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

if and only if:

$\exists n \in \N: \card A \sim \N_n$ by definition of finite set

if and only if:

$\exists n \in \N: A \sim \N_n$ by $(1)$ and Set Equivalence behaves like Equivalence Relation

if and only if:

$A$ is finite by definition of finite set.

$\blacksquare$

Sources

• Mizar article CARD_1:funcreg 8