Boolean Prime Ideal Theorem - The Ultrafilter Lemma

The Ultrafilter Lemma

A filter on a set X is a collection of nonempty subsets of X that is closed under finite intersection and under superset. An ultrafilter is a maximal filter. The ultrafilter lemma states that every filter on a set X is a subset of some ultrafilter on X (a maximal filter of nonempty subsets of X). This lemma is most often used in the study of topology. An ultrafilter that does not contain finite sets is called non-principal. The existence of non-principal ultrafilters is due to Tarski in 1930.

The ultrafilter lemma is equivalent to the Boolean prime ideal theorem, with the equivalence provable in ZF set theory without the axiom of choice. The idea behind the proof is that the subsets of any set form a Boolean algebra partially ordered by inclusion, and any Boolean algebra is representable as an algebra of sets by Stone's representation theorem.