Theorem opthwiener 1914

Description: Justification theorem for the ordered pair definition in Norbert Wiener, "A simplification of the logic of relations," Proc. of the Cambridge Philos. Soc., 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e. are not proper classes). See df-op 1815 for other ordered pair definitions.

Hypotheses

Ref	Expression
opthw.1	|- A e. V
opthw.2	|- B e. V

Assertion

Ref	Expression
opthwiener	|- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))

Proof of Theorem opthwiener

Step	Hyp	Ref	Expression
1		id 9	. . . . . . 7 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
2		snex 1859	. . . . . . . . . . . 12 |- {{B}} e. V
3	2	pri2 1842	. . . . . . . . . . 11 |- {{B}} e. {{{A}, (/)}, {{B}}}
4		eleq2 1150	. . . . . . . . . . 11 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} e. {{{A}, (/)}, {{B}}} <-> {{B}} e. {{{C}, (/)}, {{D}}}))
5	3, 4	mpbii 168	. . . . . . . . . 10 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} e. {{{C}, (/)}, {{D}}})
6	2	elpr 1823	. . . . . . . . . 10 |- ({{B}} e. {{{C}, (/)}, {{D}}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
7	5, 6	sylib 173	. . . . . . . . 9 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
8		0ex 1745	. . . . . . . . . . . . 13 |- (/) e. V
9	8	pri2 1842	. . . . . . . . . . . 12 |- (/) e. {{C}, (/)}
10		opthw.2	. . . . . . . . . . . . . 14 |- B e. V
11	10	snnz 1846	. . . . . . . . . . . . 13 |- -. {B} = (/)
12	8	elsnc 1826	. . . . . . . . . . . . . 14 |- ((/) e. {{B}} <-> (/) = {B})
13		cleqcom 1103	. . . . . . . . . . . . . 14 |- ((/) = {B} <-> {B} = (/))
14	12, 13	bitr 151	. . . . . . . . . . . . 13 |- ((/) e. {{B}} <-> {B} = (/))
15	11, 14	mtbir 167	. . . . . . . . . . . 12 |- -. (/) e. {{B}}
16		clneq2 1169	. . . . . . . . . . . 12 |- (((/) e. {{C}, (/)} /\ -. (/) e. {{B}}) -> -. {{C}, (/)} = {{B}})
17	9, 15, 16	mp2an 520	. . . . . . . . . . 11 |- -. {{C}, (/)} = {{B}}
18		cleqcom 1103	. . . . . . . . . . 11 |- ({{C}, (/)} = {{B}} <-> {{B}} = {{C}, (/)})
19	17, 18	mtbi 166	. . . . . . . . . 10 |- -. {{B}} = {{C}, (/)}
20		biorf 551	. . . . . . . . . 10 |- (-. {{B}} = {{C}, (/)} -> ({{B}} = {{D}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}})))
21	19, 20	ax-mp 6	. . . . . . . . 9 |- ({{B}} = {{D}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
22	7, 21	sylibr 175	. . . . . . . 8 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} = {{D}})
23		preq2 1871	. . . . . . . 8 |- ({{B}} = {{D}} -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
24	22, 23	syl 12	. . . . . . 7 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
25	1, 24	eqtr4d 1131	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
26		prex 1892	. . . . . . 7 |- {{A}, (/)} e. V
27		prex 1892	. . . . . . 7 |- {{C}, (/)} e. V
28	26, 27	preqr1 1872	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}} -> {{A}, (/)} = {{C}, (/)})
29	25, 28	syl 12	. . . . 5 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{A}, (/)} = {{C}, (/)})
30		snex 1859	. . . . . 6 |- {A} e. V
31		snex 1859	. . . . . 6 |- {C} e. V
32	30, 31	preqr1 1872	. . . . 5 |- ({{A}, (/)} = {{C}, (/)} -> {A} = {C})
33	29, 32	syl 12	. . . 4 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {A} = {C})
34		opthw.1	. . . . 5 |- A e. V
35	34	sneqr 1856	. . . 4 |- ({A} = {C} -> A = C)
36	33, 35	syl 12	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> A = C)
37		snex 1859	. . . . 5 |- {B} e. V
38	37	sneqr 1856	. . . 4 |- ({{B}} = {{D}} -> {B} = {D})
39	10	sneqr 1856	. . . 4 |- ({B} = {D} -> B = D)
40	22, 38, 39	3syl 21	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> B = D)
41	36, 40	jca 236	. 2 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> (A = C /\ B = D))
42		sneq 1816	. . . 4 |- (A = C -> {A} = {C})
43		preq1 1870	. . . 4 |- ({A} = {C} -> {{A}, (/)} = {{C}, (/)})
44		preq1 1870	. . . 4 |- ({{A}, (/)} = {{C}, (/)} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
45	42, 43, 44	3syl 21	. . 3 |- (A = C -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
46		sneq 1816	. . . 4 |- (B = D -> {B} = {D})
47		sneq 1816	. . . 4 |- ({B} = {D} -> {{B}} = {{D}})
48	46, 47, 23	3syl 21	. . 3 |- (B = D -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
49	45, 48	sylan9eq 1144	. 2 |- ((A = C /\ B = D) -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
50	41, 49	impbi 139	1 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))

Syntax hints:  -. wn 1   <-> wb 127   \/ wo 195   /\ wa 196   = wceq 1091   e. wcel 1092  Vcvv 1348  (/)c0 1707  {csn 1808  {cpr 1809

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812

metamath.org