Definition df-op 2416

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 2498, opprc1b 2796, opprc2 2499, and opprc3 2797). For the justifying theorem (for sets) see opth 2787. 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 2807, 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 4604, 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 3221. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opth 6666. Finally, an ordered pair of real numbers can be represented by a complex number as shown by cru 6737.

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 2411	. 2 class <.A, B>.
4	1	csn 2409	. . 3 class {A}
5	1, 2	cpr 2410	. . 3 class {A, B}
6	4, 5	cpr 2410	. 2 class {{A}, {A, B}}
7	3, 6	wceq 956	1 wff <.A, B>. = {{A}, {A, B}}

This definition is referenced by:  opeq1 2487  opeq2 2488  hbop 2496  opprc1 2498  opprc2 2499  opex 2782  elop 2783  opi1 2784  opi2 2785  opth 2787  opeqsn 2802  opeqpr 2803  uniop 2808  op1stb 2913  xpsspw 3257  relop 3275  dmsnsnsn 3329  funopg 3547  rankop 4693

Copyright terms: Public domain