# Axiom:Axiom of Choice for Finite Sets

## Axiom

Let $\SS$ be a non-empty set of finite, non-empty sets.

Then there exists a choice function for $\SS$.

## Remark

This page or section has statements made on it that ought to be extracted and proved in a Theorem page.In particular: Extract the below and put it into a theorem, no matter how trivial it may be. The "strictly weaker" statement also counts as something that ought to be stated formally.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by creating any appropriate Theorem pages that may be needed.To discuss this page in more detail, feel free to use the talk page. |

The **axiom of choice for finite sets** is trivially implied by the axiom of choice, but it is strictly weaker.

## Proof from the Ordering Principle

By the Axiom of Union, $\SS$ has a union.

Let $U = \bigcup \SS$.

By the Ordering Principle, there is a total ordering $\preceq$ on $U$.

For each $S \in \SS$, $S$ is a chain in $U$.

By Finite Non-Empty Subset of Totally Ordered Set has Smallest and Greatest Elements, each $S \in S$ has a minimum.

Let $f: \SS \to U$ be defined by:

- $\map f S = \min S$

Then $f$ is a choice function for $\SS$.

$\blacksquare$

## Proof from Hall's Marriage Theorem

Without loss of generality, suppose $\SS$ is pairwise disjoint.

This article, or a section of it, needs explaining.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

We will show that $\SS$ satisfies the **marriage condition**.

That is, for each finite subset $\FF$ of $\SS$:

- $\card \FF \le \card {\bigcup \FF}$

as follows:

Let $\FF$ be a finite subset of $\SS$.

By the Principle of Finite Choice, $\FF$ has a choice function $f_\FF: \FF \to \bigcup \FF$ such that for each $S \in \FF$, $\map {f_\FF} S \in S$.

Since $\SS$ is pairwise disjoint, $f_\FF$ is an injection.

Thus $\card \FF \le \card {\bigcup \FF}$.

By Hall's Marriage Theorem for sets of finite sets, $\SS$ has a choice function.

$\blacksquare$