Cardinality of Image of Set not greater than Cardinality of Set

Theorem

Let $X, Y$ be sets.

Let $f: X \to Y$ be a mapping.

Let $A$ be a subset of $X$.

Then:

$\card {\map {f^\to} A} \le \card A$

where $\card A$ denotes the cardinality of $A$.

Proof

By definitions of surjection and restriction of mapping:

$F \restriction_A: A \to \map {f^\to} A$ is a surjection

Thus by Surjection iff Cardinal Inequality:

$\card {\map {f^\to} A} \le \card A$

$\blacksquare$

Sources

• Mizar article CARD_1:67