Definition df-op 3246

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 3359, opprc1b 3705, opprc2 3360, and opprc3 3706). For the justifying theorem (for sets) see opth 3695. 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>._2 = {{{A}, (/)}, {{B}}}, justified by opthwiener 3717, which was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition <.A, B>._3 = {A, {A, B}} is justified by opthreg 5941, 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>._4 = ((A X. {(/)}) u. (B X. {{(/)}})), justified by opthprc 4179. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 8300. Finally, an ordered pair of real numbers can be represented by a complex number as shown by crui 8371.

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 3240	. 2 class <.A, B>.
4	1	csn 3238	. . 3 class {A}
5	1, 2	cpr 3239	. . 3 class {A, B}
6	4, 5	cpr 3239	. 2 class {{A}, {A, B}}
7	3, 6	wceq 1586	1 wff <.A, B>. = {{A}, {A, B}}

This definition is referenced by:  opeq1 3345  opeq2 3346  hbop 3354  opid 3356  opprc1 3359  opprc2 3360  opex 3690  elop 3691  opi1 3692  opi2 3693  opth 3695  opeqsn 3712  opeqpr 3713  uniop 3718  op1stb 4003  xpsspw 4223  relop 4242  dmsnsnsn 4475  funopg 4556  rankop 6040  orkurssOLD 15186  tarorpa 16046

Copyright terms: Public domain