Singleton is Finite

Theorem

Let $x$ be arbitrary.

Then $\set x$ is a finite set.

Proof

Define a mapping $f: \set x \to \N_{< 1}$:

$\map f x = 0$

By definition of singleton:

$\forall y, z \in \set x: \map f y = \map f z \implies y = z$

By definition:

$f$ is an injection.

By definition of initial segment of natural numbers:

$\N_{< 1} = \set 0$

By definition of $f$:

$\forall n \in N_{< 1}: \exists z \in \set x: \map f z = n$

By definition:

$f$ is a surjection.

By definition:

$f$ is a bijection.

By definition of set equivalence:

$\set x \sim \N_{< 1}$

Thus by definition:

$\set x$ is a finite set.

$\blacksquare$

Sources

• Mizar article FINSET_1:funcreg 1