Definition df-op 2420

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 2502, opprc1b 2802, opprc2 2503, and opprc3 2803). For the justifying theorem (for sets) see opth 2793. 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 2813, 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 4613, 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 3227. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opth 6667. Finally, an ordered pair of real numbers can be represented by a complex number as shown by cru 6738.

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 2415	. 2 class <.A, B>.
4	1	csn 2413	. . 3 class {A}
5	1, 2	cpr 2414	. . 3 class {A, B}
6	4, 5	cpr 2414	. 2 class {{A}, {A, B}}
7	3, 6	wceq 958	1 wff <.A, B>. = {{A}, {A, B}}

This definition is referenced by:  opeq1 2491  opeq2 2492  hbop 2500  opprc1 2502  opprc2 2503  opex 2788  elop 2789  opi1 2790  opi2 2791  opth 2793  opeqsn 2808  opeqpr 2809  uniop 2814  op1stb 2919  xpsspw 3263  relop 3281  dmsnsnsn 3335  funopg 3553  rankop 4703

Copyright terms: Public domain