Grothendieck Universe is Closed under Mappings

Theorem

Let $\mathbb U$ be a Grothendieck universe.

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

Let $f: u \to v$ be a mapping realized as a relation consisting of ordered pairs in Kuratowski formalization.

Then $f \in \mathbb U$.

Proof

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

By definition of mapping, we have $f \subseteq u \times v$.

Then:

\(\ds u, v\)

\(\in\)

\(\ds \mathbb U\)

\(\ds \leadsto \ \ \)

\(\ds u \times v\)

\(\in\)

\(\ds \mathbb U\)

Grothendieck Universe is Closed under Binary Cartesian Product

\(\ds \leadsto \ \ \)

\(\ds f\)

\(\in\)

\(\ds \mathbb U\)

Grothendieck Universe is Closed under Subset and $f \subseteq u \times v$

$\blacksquare$