Theorem opthwiener 3554

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 3053 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 73	. . . . . . 7 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
2		snex 3492	. . . . . . . . . . . 12 |- {{B}} e. _V
3	2	prid2 3107	. . . . . . . . . . 11 |- {{B}} e. {{{A}, (/)}, {{B}}}
4		eleq2 1958	. . . . . . . . . . 11 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} e. {{{A}, (/)}, {{B}}} <-> {{B}} e. {{{C}, (/)}, {{D}}}))
5	3, 4	mpbii 210	. . . . . . . . . 10 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} e. {{{C}, (/)}, {{D}}})
6	2	elpr 3061	. . . . . . . . . 10 |- ({{B}} e. {{{C}, (/)}, {{D}}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
7	5, 6	sylib 215	. . . . . . . . 9 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
8		0ex 3446	. . . . . . . . . . . . 13 |- (/) e. _V
9	8	prid2 3107	. . . . . . . . . . . 12 |- (/) e. {{C}, (/)}
10		opthw.2	. . . . . . . . . . . . . 14 |- B e. _V
11	10	snnz 3119	. . . . . . . . . . . . 13 |- {B} =/= (/)
12	8	elsnc 3065	. . . . . . . . . . . . . 14 |- ((/) e. {{B}} <-> (/) = {B})
13		eqcom 1886	. . . . . . . . . . . . . 14 |- ((/) = {B} <-> {B} = (/))
14	12, 13	bitri 190	. . . . . . . . . . . . 13 |- ((/) e. {{B}} <-> {B} = (/))
15	11, 14	nemtbir 2099	. . . . . . . . . . . 12 |- -. (/) e. {{B}}
16		nelneq2 1986	. . . . . . . . . . . 12 |- (((/) e. {{C}, (/)} /\ -. (/) e. {{B}}) -> -. {{C}, (/)} = {{B}})
17	9, 15, 16	mp2an 761	. . . . . . . . . . 11 |- -. {{C}, (/)} = {{B}}
18		eqcom 1886	. . . . . . . . . . 11 |- ({{C}, (/)} = {{B}} <-> {{B}} = {{C}, (/)})
19	17, 18	mtbi 208	. . . . . . . . . 10 |- -. {{B}} = {{C}, (/)}
20		biorf 807	. . . . . . . . . 10 |- (-. {{B}} = {{C}, (/)} -> ({{B}} = {{D}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}})))
21	19, 20	ax-mp 7	. . . . . . . . 9 |- ({{B}} = {{D}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
22	7, 21	sylibr 217	. . . . . . . 8 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} = {{D}})
23		preq2 3099	. . . . . . . 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 1928	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
26		prex 3526	. . . . . . 7 |- {{A}, (/)} e. _V
27		prex 3526	. . . . . . 7 |- {{C}, (/)} e. _V
28	26, 27	preqr1 3152	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}} -> {{A}, (/)} = {{C}, (/)})
29	25, 28	syl 12	. . . . 5 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{A}, (/)} = {{C}, (/)})
30		snex 3492	. . . . . 6 |- {A} e. _V
31		snex 3492	. . . . . 6 |- {C} e. _V
32	30, 31	preqr1 3152	. . . . 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 3147	. . . 4 |- ({A} = {C} -> A = C)
36	33, 35	syl 12	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> A = C)
37		snex 3492	. . . . 5 |- {B} e. _V
38	37	sneqr 3147	. . . 4 |- ({{B}} = {{D}} -> {B} = {D})
39	10	sneqr 3147	. . . 4 |- ({B} = {D} -> B = D)
40	22, 38, 39	3syl 24	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> B = D)
41	36, 40	jca 310	. 2 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> (A = C /\ B = D))
42		sneq 3054	. . . 4 |- (A = C -> {A} = {C})
43		preq1 3098	. . . 4 |- ({A} = {C} -> {{A}, (/)} = {{C}, (/)})
44		preq1 3098	. . . 4 |- ({{A}, (/)} = {{C}, (/)} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
45	42, 43, 44	3syl 24	. . 3 |- (A = C -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
46		sneq 3054	. . . 4 |- (B = D -> {B} = {D})
47		sneq 3054	. . . 4 |- ({B} = {D} -> {{B}} = {{D}})
48	46, 47, 23	3syl 24	. . 3 |- (B = D -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
49	45, 48	sylan9eq 1948	. 2 |- ((A = C /\ B = D) -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
50	41, 49	impbii 174	1 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))

Syntax hints:  -. wn 2   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300  _Vcvv 2292  (/)c0 2875  {csn 3044  {cpr 3045

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050

Copyright terms: Public domain