Grothendieck Universe is Closed under Binary Cartesian Product

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathbb U$ be a Grothendieck universe.

Let $u, v \in \mathbb U$.

Let $u \times v$ be the binary cartesian product of $u$ and $v$ realized as a set of ordered pairs in Kuratowski formalization.


Then $u \times v \in \mathbb U$.


Proof

From Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union:

$u \times v \subseteq \powerset {\powerset {u \cup v} }$

Then:

\(\ds u \cup v\) \(\in\) \(\ds \mathbb U\) Grothendieck Universe is Closed under Binary Union
\(\ds \leadsto \ \ \) \(\ds \powerset {u \cup v}\) \(\in\) \(\ds \mathbb U\) Grothendieck Universe: Axiom (3)
\(\ds \leadsto \ \ \) \(\ds \powerset {\powerset {u \cup v} }\) \(\in\) \(\ds \mathbb U\) Grothendieck Universe: Axiom (3)
\(\ds \leadsto \ \ \) \(\ds u \times v\) \(\in\) \(\ds \mathbb U\) Grothendieck Universe is Closed under Subset

$\blacksquare$