# Equivalence of Definitions of Ordered Pair

## Theorem

The following definitions of the concept of **Ordered Pair** are equivalent:

### Informal Definition

An **ordered pair** is a two-element set together with an ordering.

In other words, one of the elements *is* distinguished above the other - it comes first.

Such a structure is written:

- $\tuple {a, b}$

and it means:

**first $a$, then $b$**.

### Kuratowski Formalization

The concept of an ordered pair can be formalized by the definition:

- $\tuple {a, b} := \set {\set a, \set {a, b} }$

This formalization justifies the existence of ordered pairs in Zermelo-Fraenkel set theory.

## Proof

### Equality of Ordered Pairs

From Equality of Ordered Pairs, we have that:

- $\set {\set a, \set {a, b} } = \set {\set c, \set {c, d} } \iff a = c, b = d$

hence showing that the Kuratowski formalization fulfils the requirement for equality.

### Existence of Cartesian Product

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

- $A \times B \subseteq \powerset {\powerset {A \cup B} }$

By Axiom of Specification, there is a set $C$ where:

- $C = \set {x \in \powerset {\powerset {A \cup B} } : x \in A \times B}$

Thus, the cartesian product exists.

By Cartesian Product is Unique, the cartesian product is unique.

$\blacksquare$

## Sources

- 1964: W.E. Deskins:
*Abstract Algebra*... (previous) ... (next): Exercise $1.2: \ 12$ - 1972: A.G. Howson:
*A Handbook of Terms used in Algebra and Analysis*... (previous) ... (next): $\S 2$: Sets and functions: Graphs and functions