Definition df-op 2406

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 2489, opprc1b 2786, opprc2 2490, and opprc3 2787). For the justifying theorem (for sets) see opth 2777. 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 2796, 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 4576, 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 3211. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opth 6596. Finally, an ordered pair of real numbers can be represented by a complex number as shown by cru 6667.

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 2401	. 2 class <.A, B>.
4	1	csn 2399	. . 3 class {A}
5	1, 2	cpr 2400	. . 3 class {A, B}
6	4, 5	cpr 2400	. 2 class {{A}, {A, B}}
7	3, 6	wceq 953	1 wff <.A, B>. = {{A}, {A, B}}

This definition is referenced by:  opeq1 2478  opeq2 2479  hbop 2487  opprc1 2489  opprc2 2490  opex 2772  elop 2773  opi1 2774  opi2 2775  opth 2777  opeqsn 2791  opeqpr 2792  uniop 2797  op1stb 2903  xpsspw 3247  relop 3265  dmsnsnsn 3318  funopg 3533  rankop 4665

Copyright terms: Public domain