Proof of Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set

Membership. Let $u$ and $v$ be sets; $(u,v)$ is a set by The Ordered Pair of Two Sets and Nested Tuples §pair. By The Cartesian Product of Two Classes §product, unfolding the class abstraction by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction (class abstractions are unfolded without further mention below), $(u,v)\in X\times Y$ holds if and only if there are sets $u'$ and $v'$ with $u'\in X$, $v'\in Y$ and $(u,v)=(u',v')$. If $u\in X$ and $v\in Y$, take $u'=u$ and $v'=v$. Conversely, given such $u'$ and $v'$, The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic yields $u=u'$ and $v=v'$, so $u\in X$ and $v\in Y$.

Set. Let $x$ and $y$ be sets. By Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §binary-union the union $x\cup y$ is a set, so by The Union Set and the Power Set of a Set §power the power sets $\mathcal{P}(x\cup y)$ and $\mathcal{P}(\mathcal{P}(x\cup y))$ exist. Let $p\in x\times y$. By The Cartesian Product of Two Classes §product there are sets $u\in x$ and $v\in y$ with $p=(u,v)=\{\{u\},\{u,v\}\}$, by The Ordered Pair of Two Sets and Nested Tuples §pair. The only element of $\{u\}$ is $u$, by The Empty Set, the Unordered Pair and the Singleton §singleton, and the elements of $\{u,v\}$ are $u$ and $v$, by The Empty Set, the Unordered Pair and the Singleton §pair; since $u\in x$ and $v\in y$, both lie in $x\cup y$ by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations. Hence $\{u\}$ and $\{u,v\}$ are subsets of $x\cup y$, that is, elements of $\mathcal{P}(x\cup y)$ by The Union Set and the Power Set of a Set §power. The elements of $p$ are exactly $\{u\}$ and $\{u,v\}$ (The Empty Set, the Unordered Pair and the Singleton §pair), so $p\subseteq\mathcal{P}(x\cup y)$ and therefore $p\in\mathcal{P}(\mathcal{P}(x\cup y))$, again by The Union Set and the Power Set of a Set §power. As $p$ was arbitrary, $x\times y\subseteq\mathcal{P}(\mathcal{P}(x\cup y))$ by Subclasses and Subsets §subclass, and $x\times y$ is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass.