\documentclass{article}

\usepackage[english]{babel}

\usepackage{amsmath}
% for symbols such as /implies
\usepackage{amssymb}
% for symbols such as /subsetneq
\usepackage{amsthm}
% for commands such as \newtheorem

\theoremstyle{definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{axiom}{Axiom}

\begin{document}

\section{Axiom of Choice}

\begin{axiom}[Axiom of Choice]
  For any collection of nonempty sets $\mathcal{A}$, there exists a function $f:\mathcal{A}\to\cup\mathcal{A}$ such that if $A\in\mathcal{A}$ then $f(A)\in A$.
  $$
    \forall \mathcal{A} \ \forall A \ (A\in\mathcal{A} \implies A\neq\emptyset) \implies
    \exists f \ (f \subseteq \mathcal{A} \times \cup\mathcal{A} \land (A\in\mathcal{A} \implies \exists!y \ (((A,y)\in f) \land (y\in A))))
  $$
\end{axiom}

\begin{axiom}[Well-Ordering Theorem]
  For any set $X$, there exists a relation $\leq$ on $X$ such that $(X,\leq)$ is a well-ordered set.
\end{axiom}

\begin{axiom}[Zorn's Lemma]
  If $(X,\leq)$ is a partially ordered set such that every totally ordered subset $C\subseteq X$ has an upper bound in $X$, then $X$ contains a maximal element.
\end{axiom}

\begin{theorem}
  The following are equivalent.
  \begin{enumerate}
    \item Axiom of Choice
    \item Well-Ordering Theorem
    \item Zorn's Lemma
  \end{enumerate}
  \begin{proof}
    WIP

    Suppose the well-ordering theorem is true. Let $\mathcal{A}$ be a collection of nonempty sets. By the well-ordering theorem, there is a relation $\leq$ on $\cup\mathcal{A}$ such that $(\cup\mathcal{A}, \leq)$ is a well-ordered set. Let 
    $$
      f = \{(X,y)\in\mathcal{A}\times\cup\mathcal{A} : y \text{ is the smallest element of } X\}
    $$
    Let $A\in\mathcal{A}$. Then $A\subseteq\cup\mathcal{A}$. Since $\cup\mathcal{A}$ is well-ordered, $A$ has a minimal element $a\in A$. Then $(A,a)\in\mathcal{A}\times\cup\mathcal{A}$. Since a well-ordered set is totally ordered, $a$ is the smallest element of $A$. Since smallest elements are unique, it follows that $a$ is a unique element such that $(A,a)\in f$. Since $\mathcal{A}$ and $A\in\mathcal{A}$ are arbitrary, the Axiom of Choice follows.
  \end{proof}
\end{theorem}

\begin{axiom}[Alternate Axiom of Choice]
  For any collection of nonempty pairwise disjoint sets $\mathcal{A}$, there exists a set $B\subseteq\cup\mathcal{A}$ such that for each $A\in\mathcal{A}$, there is a unique $b\in B$ such that $b\in A$.
\end{axiom}


    
\end{document}