Definition df-op 2474

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 2563, opprc1b 2872, opprc2 2564, and opprc3 2873). For the justifying theorem (for sets) see opth 2863. 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 2884, 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 4749, 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 × {∅}) ∪ (B × {{∅}})), justified by opthprc 3306. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 6867. Finally, an ordered pair of real numbers can be represented by a complex number as shown by crui 6938.

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

This definition is referenced by:  opeq1 2552  opeq2 2553  hbop 2561  opprc1 2563  opprc2 2564  opex 2858  elop 2859  opi1 2860  opi2 2861  opth 2863  opeqsn 2879  opeqpr 2880  uniop 2885  op1stb 3136  xpsspw 3346  relop 3365  dmsnsnsn 3578  funopg 3652  rankop 4839

Copyright terms: Public domain