\begin{definition}[Definition:Grothendieck Universe]
A '''Grothendieck universe''' is a set (not a class) which has the properties expected of the universe $\mathbb U$ of sets in the sense of the Zermelo-Fraenkel axioms with the following properties:
:$(1): \quad \mathbb U$ is a transitive set: If $u \in \mathbb U$ and $x \in u$ then $x \in \mathbb U$
:$(2): \quad$ If $ u, v \in \mathbb U$ then $\set {u, v} \in \mathbb U$
:$(3): \quad$ If $u \in \mathbb U$ then the power set $\powerset u \in \mathbb U$
:$(4): \quad$ If $A \in \mathbb U$, and $\set {u_\alpha: \alpha \in A}$ is a family of elements $u_\alpha \in \mathbb U$ indexed by $A$, then $\ds \bigcup_{\alpha \mathop \in A} u_\alpha \in \mathbb U$
\end{definition}