The Ordered Pair of Two Sets and Nested Tuples

¶ For sets $x$ and $y$, the ordered pair of $x$ and $y$ is the set

$$(x,y)=\bigl\{\{x\},\{x,y\}\bigr\},$$

the unordered pair of the singleton $\{x\}$ and the unordered pair $\{x,y\}$. Its first component is $x$ and its second component is $y$.

The ordered pair is a defined set symbol.

¶ This clause is a notation scheme of the metatheory, one notation for each number of entries. For a metatheoretic number $n\ge1$ and sets $x_{1},\dots,x_{n}$, the tuple $\langle x_{1},\dots,x_{n}\rangle$ is defined by recursion on $n$:

$$\langle x_{1}\rangle=x_{1},\qquad \langle x_{1},\dots,x_{n},x_{n+1}\rangle=\bigl(\langle x_{1},\dots,x_{n}\rangle,x_{n+1}\bigr).$$

Thus $\langle x,y\rangle=(x,y)$ and $\langle u,v,w\rangle=((u,v),w)$; each tuple is a set, being either $x_{1}$ or an ordered pair, and a tuple stands for the nested ordered-pair expression it abbreviates, so that its occurrences are eliminated as those of ordered pairs.