Subset of Cartesian Product

Theorem

Let $S$ be a set of ordered pairs.

Then $S$ is the subset of the cartesian product of two sets.

Let $S$ be a set of ordered pairs.

Let $x \in S$ such that $x = \set {\set a, \set {a, b} }$ as defined in Kuratowski Formalization of Ordered Pair.

Since the elements of $S$ are sets, we can form the union $\mathbb S = \bigcup S$ of the sets in $S$.

Since $x \in S$ it follows that the elements of $x$ are elements of $\mathbb S$.

Since $\set {a, b} \in x$ it follows that $\set {a, b} \in \mathbb S$.

Now we can form the union $\mathbb S' = \bigcup \mathbb S$ of the sets in $\mathbb S$.

Since $\set {a, b} \in \mathbb S$ it follows that both $a$ and $b$ are elements of $\mathbb S' = \bigcup \bigcup S$.

Thus from the Kuratowski Formalization of Ordered Pair we have that $S$ is a subset of some $A \times B$.

We can at this stage take both $A$ and $B$ as being equal to $\bigcup \bigcup S$.

Finally, the axiom of specification is applied to construct the sets:

$A = \set {a: \exists b: \tuple {a, b} \in S}$

and

$B = \set {b: \exists a: \tuple {a, b} \in S}$

$A$ and $B$ are seen to be the first and second projections respectively of $S$.

$\blacksquare$