Metamath Proof Explorer


Table of Contents - 20.16.5.15. Tuples of classes

This subsection gives a definition of an ordered pair, or couple (2-tuple), that "works" for proper classes, as evidenced by Theorems bj-2uplth and bj-2uplex, and more importantly, bj-pr21val and bj-pr22val. In particular, one can define well-behaved tuples of classes. Classes in ZF(C) are only virtual, and in particular they cannot be quantified over. Theorem bj-2uplex has advantages: in view of df-br, several sethood antecedents could be removed from existing theorems. For instance, relsnopg (resp. relsnop) would hold without antecedents (resp. hypotheses) thanks to relsnb). Also, the antecedent could be removed from brrelex12 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct could be simplified by removing the exception currently made for the empty set.

The projections are denoted by and and the couple with projections (or coordinates) and is denoted by .

Note that this definition uses the Kuratowski definition (df-op) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg) without needing the axiom of regularity; it could even bypass this definition by "inlining" it.

This definition is due to Anthony Morse and is expounded (with idiosyncratic notation) in

Anthony P. Morse, A Theory of Sets, Academic Press, 1965 (second edition 1986).

Note that this extends in a natural way to tuples.

A variation of this definition is justified in opthprc, but here we use "tagged versions" of the factors (see df-bj-tag) so that an m-tuple can equal an n-tuple only when m = n (and the projections are the same).

A comparison of the different definitions of tuples (strangely not mentioning Morse's), is given in

Dominic McCarty and Dana Scott, Reconsidering ordered pairs, Bull. Symbolic Logic, Volume 14, Issue 3 (Sept. 2008), 379--397.

where a recursive definition of tuples is given that avoids the 2-step definition of tuples and that can be adapted to various set theories.

Finally, another survey is

Akihiro Kanamori, The empty set, the singleton, and the ordered pair, Bull. Symbolic Logic, Volume 9, Number 3 (Sept. 2003), 273--298. (available at http://math.bu.edu/people/aki/8.pdf)

  1. bj-cproj
  2. df-bj-proj
  3. bj-projeq
  4. bj-projeq2
  5. bj-projun
  6. bj-projex
  7. bj-projval
  8. bj-c1upl
  9. df-bj-1upl
  10. bj-1upleq
  11. bj-cpr1
  12. df-bj-pr1
  13. bj-pr1eq
  14. bj-pr1un
  15. bj-pr1val
  16. bj-pr11val
  17. bj-pr1ex
  18. bj-1uplth
  19. bj-1uplex
  20. bj-1upln0
  21. bj-c2uple
  22. df-bj-2upl
  23. bj-2upleq
  24. bj-pr21val
  25. bj-cpr2
  26. df-bj-pr2
  27. bj-pr2eq
  28. bj-pr2un
  29. bj-pr2val
  30. bj-pr22val
  31. bj-pr2ex
  32. bj-2uplth
  33. bj-2uplex
  34. bj-2upln0
  35. bj-2upln1upl