Definition df-op 2473

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 (see opprc1 2562, opprc1b 2871, opprc2 2563, and opprc3 2872). For the justifying theorem (for sets) see opth 2862. 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 2883, 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 4747, 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 X. {(/)}) u. (B X. {{(/)}})), justified by opthprc 3305. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 6865. Finally, an ordered pair of real numbers can be represented by a complex number as shown by crui 6936.

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 2468	. 2 class <.A, B>.
4	1	csn 2466	. . 3 class {A}
5	1, 2	cpr 2467	. . 3 class {A, B}
6	4, 5	cpr 2467	. 2 class {{A}, {A, B}}
7	3, 6	wceq 991	1 wff <.A, B>. = {{A}, {A, B}}

This definition is referenced by:  opeq1 2551  opeq2 2552  hbop 2560  opprc1 2562  opprc2 2563  opex 2857  elop 2858  opi1 2859  opi2 2860  opth 2862  opeqsn 2878  opeqpr 2879  uniop 2884  op1stb 3135  xpsspw 3345  relop 3364  dmsnsnsn 3577  funopg 3651  rankop 4837

Copyright terms: Public domain