Unordered Pair is Finite

Theorem

Let $x, y$ be arbitrary.

Then $\set {x, y}$ is finite.

Proof

By Union of Disjoint Singletons is Doubleton:

$\set {x, y} = \set x \cup \set y$

By Singleton is Finite:

$\set x$ and $\set y$ are finite.

Thus by Union of Finite Sets is Finite:

$\set {x, y}$ is finite.

$\blacksquare$

Sources

• Mizar article FINSET_1:funcreg 2