\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{Sets}

\begin{definition}
  A \emph{set} is a collection of \emph{elements}.
\end{definition}

Let $S$ be a set. 
To denote that $x$ is an element of $S$, we write $x \in S$.
To denote that $x$ is not an element of $S$, we write $x \notin S$.
If $S$ contains only a few elements, we may denote it by listing its elements surrounded by brackets.
For instance, if $S$ has elements $a$, $b$, and $c$, we write $S = \{a,b,c\}$. 

\begin{example}
  \begin{align*}
    \mathbb{N} &= \{0, 1, 2, \dots \} \\
    \mathbb{Z}_+ &= \{1, 2, 3, \dots \} \\
    \mathbb{Z} &= \{\dots, -1, 0, 1, \dots \} \\
    \mathbb{Q} &= \left\{\frac{a}{b} : a,b \in \mathbb{Z} \land b \neq 0 \right\}
  \end{align*}
\end{example}

\begin{definition}
  A set $A$ is a \emph{subset} of a set $S$ if every element of $A$ is an element of $S$.
  This is denoted as $A \subseteq S$. That is,
  $$
    A \subseteq S \iff \forall x (x \in A \implies x \in S)
  $$
  We may also write $S \supseteq A$ to say $S$ \emph{contains} $A$ whenever $A \subseteq S$.
  We have
  $$
    S \supseteq A \iff A \subseteq S
  $$
\end{definition}

\begin{definition}
  Sets $A$ and $S$ are \emph{equal} if both $A \subseteq S$ and $S \subseteq A$. 
  This is denoted as $A = S$. That is,
  $$
    A = S \iff (A \subseteq S) \land (S \subseteq A)
  $$
  Sets $A$ and $S$ are \emph{unequal} if they are not equal, denoted $A \neq S$. That is,
  $$
    A \neq S \iff \lnot (A = S)
  $$
\end{definition}

\begin{definition}
  A set $A$ is a \emph{proper subset} of a set $S$ if $A \subseteq S$ and $A \neq S$.
  This is denoted as $A \subset S$. That is,
  $$
    A \subset S \iff (A \subseteq S) \land (A \neq S)
  $$
  We may also write $S \supset A$ to say $S$ \emph{properly contains} $A$ whenever $A \subset S$.
  We have
  $$
    S \supset A \iff A \subset S
  $$
\end{definition}

Formal treatment of sets is done with ZF set theory, which involves the following axioms:

\begin{axiom}[Axiom of extensionality]
  Two sets are equal if they have the same elements.
  $$
    \forall x \forall y [\forall z (z \in x \iff z \in y) \implies x = y]
  $$
\end{axiom}

\begin{axiom}[Axiom of regularity (foundation)]
  Every non-empty set $x$ contains a member $y$ such that $x$ and $y$ are disjoint sets.
  $$
    \forall x [(\exists a (a \in x)) \implies \exists y (y \in x \land \lnot \exists z (z \in y \land z \in x))]
  $$
  Equivalently,
  $$
    \forall x (x \neq \emptyset \implies \exists y (y \in x \land y \cap x = \emptyset))
  $$
\end{axiom}

\begin{axiom}[Axiom schema of specification (separation, restricted comprehension)]
  $$
    \forall z \forall w_1 \forall w_2 \dots \forall w_n \exists y \forall x [x \in y \iff ((x \in z) \land \varphi(x, w_1, w_2, \dots, w_n, z))]
  $$
\end{axiom}

\begin{axiom}[Axiom of pairing]
  If $x$ and $y$ are sets, there exists a set containing $x$ and $y$ as elements.
  $$
    \forall x \forall y \exists z ((x \in z) \land (y \in z))
  $$
\end{axiom}

\begin{axiom}[Axiom of union]
  For any set of sets $\mathcal{F}$, there is a set containing every element that is a member of some member of $\mathcal{F}$.
  $$
    \forall \mathcal{F} \exists A \forall Y \forall x [(x \in Y \land Y \in \mathcal{F}) \implies x \in A]
  $$
  The union $\cup \mathcal{F}$ is constructed using the axiom of specification:
  $$
    \cup \mathcal{F} = \{x \in A : \exists Y (x \in Y \land Y \in \mathcal{F})\}
  $$
\end{axiom}

\begin{axiom}[Axiom schema of replacement]
  The image of a set under any definable function will also fall inside a set.
  $$
    \forall A \forall w_1 \forall w_2 \dots \forall w_n [\forall x (x \in A \implies \exists ! y \varphi) \implies \exists B \forall x (x \in A \implies \exists y (y \in B \land \varphi))]
  $$
\end{axiom}

\begin{axiom}[Axiom of infinity]
  Let $S(w) = w \cup \{w\}$.
  $$
        \exists X [\exists e (\forall z \lnot (z \in e) \land e \in X) \land \forall y (y \in X \implies S(y) \in X)]
  $$
  Equivalently,
  $$
    \exists X [\emptyset \in X \land \forall y (y \in X \implies S(y) \in X)]
  $$
\end{axiom}

\begin{axiom}[Axiom of power set]
  First, define \emph{subset}.
  $$
    (z \subseteq x) \iff (\forall q (q \in z \implies q \in x))
  $$
  For any set $x$, there is a set $y$ that contains every subset of $x$.
  $$
    \forall x \exists y \forall z (z \subseteq x \implies z \in y)
  $$
  The power set $\mathcal{P}(x)$ is constructed using the axiom of specification:
  $$      
    \mathcal{P}(x) = \{z \in y : z \subseteq x \}
  $$
\end{axiom}

\begin{axiom}[Axiom of well-ordering (choice)]
  For any set $X$, there exists a binary relation $R$ which well-orders $X$.
\end{axiom}
    
\end{document}