Use the Kuratowski ordered pairThe axiom of pairing first produces by pairing with itself, then , and then the pair of these two sets. The axiom of extensionality supplies the usual uniqueness of each specified set. In particular, no use of Axiom schema of replacement is needed to construct a single ordered pair from two given sets.
To recover the coordinates from , observe thatThe first equality recovers . Once is known, the second recovers : if its union is the singleton then , and otherwise is its unique element different from . Hence equality of two encoded pairs forces equality of both coordinates, including the degenerate case .
The first ordered triple encoding works. Ifinjectivity of the ordered pair construction first gives and , and a second application gives and . The construction uses only two successive ordered pair constructions, so is a set as well.
Articles by others on the same topic
There are currently no matching articles.