Definition df-op 1815

Description: Kuratowski's ordered pair definition. Definition 9.1 of [Quine] p. 58. For proper classes it is not meaningful but is well-defined and we allow it for convenience. For the justifying theorem (for sets) see opth 1898. There are other ways to define ordered pairs; the basic requirement is that two ordered pairs are equal iff their respective members are equal. In 1914 Norbert Wiener gave the first successful definition ⟨A, B⟩₁ = {{{A}, ∅}, {{B}}}, justified by opthwiener 1914, which was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition ⟨A, B⟩₂ = {A, {A, B}} is justified by opthreg 3455, but it requires the Axiom of Regularity for its justification and is not commonly used. A definition that also works for proper classes is ⟨A, B⟩₃ = ((A × {∅}) ∪ (B × {{∅}})), justified by opthprc 2457. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opth 4724. Finally, an ordered pair of real numbers can be represented by a complex number as shown by cru 4529.

Assertion

Ref	Expression
df-op	⊢ ⟨A, B⟩ = {{A}, {A, B}}

Detailed syntax breakdown of Definition df-op

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cop 1810	. 2 class ⟨A, B⟩
4	1	csn 1808	. . 3 class {A}
5	1, 2	cpr 1809	. . 3 class {A, B}
6	4, 5	cpr 1809	. 2 class {{A}, {A, B}}
7	3, 6	wceq 1091	1 wff ⟨A, B⟩ = {{A}, {A, B}}

This definition is referenced by:  opeq1 1876  opeq2 1877  hbop 1879  opex 1893  elop 1894  opi1 1895  opi2 1896  opth 1898  opprc1 1905  opprc2 1907  unop 1931  op1stb 1992  xpex 2488  dmsnsnsn 2548

metamath.org