Theorem: Stone's Representation Theorem for Boolean Algebras

Let $B$ be a Boolean algebra.
Let $S$ be the Stone space of $B$.
Then:
:The set of clopen sets in $S$ is a Boolean algebra under union, intersection, and complementation in $S$.
:That Boolean algebra is isomorphic to $B$.

Proof:
{{Proofread}}
{{Explain| Explain how the Ultrafilter Lemma/Boolean prime ideal theorem or Axiom of choice/Zorn's Lemma is explicitly used in the proof.}}
First, the statement of the proof has to be shown to be equivalent to the form:
Let $B$ be a Boolean algebra.
This proof will assume the Ultrafilter Lemma holds.
Then there exists a set $X$ and a bijection:
:$\phi: B \to \powerset X$
where $\powerset X$ denotes the power set of $X$, such that for all $a, b \in B$:
:$\map \phi {\neg a} = X \setminus \map \phi a$, where $\neg a$ denotes the complement of $a$ in $B$
:$\map \phi {a \wedge b} = \map \phi a \cap \map \phi b$ and $\map \phi {a \vee b} = \map \phi a \cup \map \phi b$
Furthermore, the ordering on $B$ induced by inclusion is isomorphic to the partial ordering on $\powerset X$ induced by inclusion.
...because the above is nothing like the statement of the problem as put together by the original author of this page.
{{Explain| How is the statement "...because the above is nothing like the statement of the problem as put together by the original author of this page." related to the proof?<br/>Because it is not trivially obvious that one is the same as the other. Until this has been formatted and the links included it is far from easy to read it.}}
Let $B$ be a Boolean algebra.
Define $X$ to be the set of all ultrafilters of $B$, that is, the maximal filters containing no proper filter.
We claim that $\phi : B \to \powerset X$ defined by:
:$\map \phi a = {F \in X : a \in F}$
is the desired bijection.
First, we show that $\phi$ is a well-defined function.
Let $a \in B$.
Since $B$ is a Boolean algebra, it is a distributive lattice.
so the set of all filters containing $a$ is closed under finite intersections and unions.
Let $\FF_a$ denote the set of all filters containing $a$.
Since $B$ is a Boolean algebra, it has a least element $\bot$, which is contained in every filter.
So $\FF_a$ is nonempty.
Furthermore, if $\FF$ is a proper filter containing $a$, then $\FF$ is not maximal.
So there exists a filter $\GG$ containing $\FF$ and not containing $a$.
But then $\GG$ contains $\neg a$.
So $\GG$ is not in $\FF_a$.
Therefore, $\FF_a$ is a proper filter containing $a$.
Hence $\FF_a$ is an ultrafilter.
Next, we show that $\phi$ is injective. 
Let $a, b \in B$ such that:
:$\map \phi a = \map \phi b$.
Then for all $F \in X$, we have:
:$a \in F \iff b \in F$
In particular, if $F$ is an ultrafilter containing $a$, then $F$ contains $b$, so $a \le b$.
Similarly, if $F$ is an ultrafilter containing $b$, then $F$ contains $a$, so $b \le a$. 
Therefore:
:$a = b$
and hence $\phi$ is injective.
To show that $\phi$ is surjective, let:
:$A \subseteq X$
Define:
:$\ds a = \bigwedge_{F \mathop \in A} F$
where the intersection is taken in $B$. 
Since $B$ is a Boolean algebra, it is complete, so the infimum of any subset of $B$ exists. 
We claim that:
:$\map \phi a = A$
To see this, let $F \in X$.
Then $F$ is an ultrafilter, so:
:$a \in F \lor \neg a \in F$
If $a \in F$, then $F$ contains every element of $A$.
So:
:$F \in \map \phi a$
If:
:$\neg a \in F$
then for each $G \in A$, we have:
:$G \nsubseteq F$
so:
:$F \in \map \phi {\neg G}$
But then:
:$F \in \map \phi {\bigvee_{G \in A} \neg G} = \map \phi {\neg a}$
so:
:$F \notin \map \phi a$
Therefore:
:$\map \phi a = A$
and hence $\phi$ is surjective.
Finally, we show that $\phi$ preserves the Boolean algebra operations and the order relation.
Let $a, b \in B$.
Then for all $F \in X$:
{{begin-eqn}}
{{eqn | l = F
      | o = \in
      | r = \map \phi {\neg a}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \neg a
      | o = \in
      | r = F
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a
      | o = \notin
      | r = F
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = F
      | o = \in
      | r = \relcomp X {\map \phi a}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = F
      | o = \in
      | r = X \setminus \map \phi a
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = F
      | o = \in
      | r = \map \phi {\neg \map \phi a}
      | c = 
}}
{{end-eqn}}
Therefore:
:$\map \phi {\neg a} = X \setminus \map \phi a$
Similarly, for all $F \in X$:
{{begin-eqn}}
{{eqn | l = F
      | o = \in
      | r = \map \phi {a \wedge b}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a \wedge b
      | o = \in
      | r = F
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a, b
      | o = \in
      | r = F
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = F
      | o = \in
      | r = \map \phi a \cap \map \phi b
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = F
      | o = \in
      | r = \map \phi {a \wedge b}
      | c = 
}}
{{end-eqn}}
Therefore:
:$\map \phi {a \wedge b} = \map \phi a \cap \map \phi b$
Similarly, for all $F \in X$:
{{begin-eqn}}
{{eqn | l = F
      | o = \in
      | r = \map \phi {a \vee b}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a \vee b
      | o = \in
      | r = F
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a
      | o = \in
      | r = F
      | c = 
}}
{{eqn | lo= \text {or}
      | l = b
      | o = \in
      | r = F
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = F
      | o = \in
      | r = \map \phi a \cup \map \phi b
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = F
      | o = \in
      | r = \map \phi {a \vee b}
      | c = 
}}
{{end-eqn}}
Therefore:
:$\map \phi {a \vee b} = \map \phi a \cup \map \phi b$
Finally, to show that $\phi$ preserves the order relation, let $a, b \in B$.
Then:
:$a \le b$
{{iff}}:
:$a \wedge \neg b = \bot$
Therefore, for all $F \in X$:
{{begin-eqn}}
{{eqn | l = F
      | o = \in
      | r = \map \phi a
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a 
      | o = \in
      | r = F
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a \wedge \neg b
      | o = \notin
      | r = F
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = b
      | o = \in
      | r = F
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = F
      | o = \in
      | r = \map \phi b
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \phi a
      | o = \subseteq
      | r = \map \phi b
      | c = 
}}
{{end-eqn}}
Therefore, $\phi$ preserves the order relation. This completes the proof.
{{qed}}
{{explain|A lot still to unpack in all of the above. Separate statements of the subresults would help, so as to explain to the novice exactly what is being proved and how what is being demonstrated proves that thing. Justification for every step by means of links to every result used still needs to be provided.}}
{{Namedfor|Marshall Harvey Stone|cat = Stone}}