Editing Ordered pair (section)

====Proving that definitions satisfy the characteristic property====
Prove: (''a'', ''b'') = (''c'', ''d'') [[if and only if]] ''a'' = ''c'' and ''b'' = ''d''.

'''Kuratowski''':<br>
''If''. If ''a'' = ''c'' and ''b'' = ''d'', then {{''a''}, {''a'', ''b''}} = {{''c''}, {''c'', ''d''}}. Thus (''a, b'')<sub>K</sub> = (''c'', ''d'')<sub>K</sub>.

''Only if''. Two cases: ''a'' = ''b'', and ''a'' ≠ ''b''.

If ''a'' = ''b'':
:(''a, b'')<sub>K</sub> = {{''a''}, {''a'', ''b''}}  = {{''a''}, {''a'', ''a''}} = <nowiki>{{</nowiki>''a''}}.
:{{''c''}, {''c'', ''d''}} = (''c'', ''d'')<sub>K</sub> = (''a'', ''b'')<sub>K</sub> = <nowiki>{{</nowiki>''a''}}.
:Thus {''c''} = {''c'', ''d''} = {''a''}, which implies ''a'' = ''c'' and ''a'' = ''d''. By hypothesis, ''a'' = ''b''. Hence ''b'' = ''d''.

If ''a'' ≠ ''b'', then (''a'', ''b'')<sub>K</sub> = (''c'', ''d'')<sub>K</sub> implies {{''a''}, {''a'', ''b''}} = {{''c''}, {''c'', ''d''}}.

:Suppose {''c'', ''d''} = {''a''}. Then ''c'' = ''d'' = ''a'', and so {{''c''}, {''c'', ''d''}} = {{''a''}, {''a'', ''a''}} = {{''a''}, {''a''}} = <nowiki>{{</nowiki>''a''}}. But then {{''a''}, {''a, b''}} would also equal <nowiki>{{</nowiki>''a''}}, so that ''b'' = ''a'' which contradicts ''a'' ≠ ''b''.

:Suppose {''c''} = {''a'', ''b''}. Then ''a'' = ''b'' = ''c'', which also contradicts ''a'' ≠ ''b''.

:Therefore {''c''} = {''a''}, so that ''c = a'' and {''c'', ''d''} = {''a'', ''b''}.

:If ''d'' = ''a'' were true, then {''c'', ''d''} = {''a'', ''a''} = {''a''} ≠ {''a'', ''b''}, a contradiction. Thus ''d'' = ''b'' is the case, so that ''a'' = ''c'' and ''b'' = ''d''.

'''Reverse''':<br>
(''a, b'')<sub>reverse</sub> = {{''b''}, {''a, b''}} = {{''b''}, {''b, a''}} = (''b, a'')<sub>K</sub>.

''If''. If (''a, b'')<sub>reverse</sub> = (''c, d'')<sub>reverse</sub>,
(''b, a'')<sub>K</sub> = (''d, c'')<sub>K</sub>. Therefore, ''b = d'' and ''a = c''.

''Only if''. If ''a = c'' and ''b = d'', then {{''b''}, {''a, b''}} = {{''d''}, {''c, d''}}.
Thus (''a, b'')<sub>reverse</sub> = (''c, d'')<sub>reverse</sub>.

'''Short:'''<ref>For a formal [[Metamath]] proof of the adequacy of '''short''', see [http://us.metamath.org/mpegif/opthreg.html here (opthreg).] Also see Tourlakis (2003), Proposition III.10.1.</ref>

''If'': If ''a = c'' and ''b = d'', then {''a'', {''a, b''}} = {''c'', {''c, d''}}. Thus (''a, b'')<sub>short</sub> = (''c, d'')<sub>short</sub>.

''Only if'': Suppose {''a'', {''a, b''}} = {''c'', {''c, d''}}.
Then ''a'' is in the left hand side, and thus in the right hand side.
Because equal sets have equal elements, one of ''a = c'' or ''a'' = {''c, d''} must be the case.
:If ''a'' = {''c, d''}, then by similar reasoning as above, {''a, b''} is in the right hand side, so {''a, b''} = ''c'' or {''a, b''} = {''c, d''}.
::If {''a, b''} = ''c'' then ''c'' is in {''c, d''} = ''a'' and ''a'' is in ''c'', and this combination contradicts the axiom of regularity, as {''a, c''} has no minimal element under the relation "element of."
::If {''a, b''} = {''c, d''}, then ''a'' is an element of ''a'', from ''a'' = {''c, d''} = {''a, b''}, again contradicting regularity.
:Hence ''a = c'' must hold.

Again, we see that {''a, b''} = ''c'' or {''a, b''} = {''c, d''}.
:The option {''a, b''} = ''c'' and ''a = c'' implies that ''c'' is an element of ''c'', contradicting regularity.
:So we have ''a = c'' and {''a, b''} = {''c, d''}, and so: {''b''} = {''a, b''} \ {''a''} = {''c, d''} \ {''c''} = {''d''}, so ''b'' = ''d''.