Theorem opthwiener 2884

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 2474 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 59	. . . . . . 7 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
2		snex 2826	. . . . . . . . . . . 12 |- {{B}} e. V
3	2	prid2 2514	. . . . . . . . . . 11 |- {{B}} e. {{{A}, (/)}, {{B}}}
4		eleq2 1578	. . . . . . . . . . 11 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} e. {{{A}, (/)}, {{B}}} <-> {{B}} e. {{{C}, (/)}, {{D}}}))
5	3, 4	mpbii 191	. . . . . . . . . 10 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} e. {{{C}, (/)}, {{D}}})
6	2	elpr 2482	. . . . . . . . . 10 |- ({{B}} e. {{{C}, (/)}, {{D}}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
7	5, 6	sylib 196	. . . . . . . . 9 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
8		0ex 2785	. . . . . . . . . . . . 13 |- (/) e. V
9	8	prid2 2514	. . . . . . . . . . . 12 |- (/) e. {{C}, (/)}
10		opthw.2	. . . . . . . . . . . . . 14 |- B e. V
11	10	snnz 2522	. . . . . . . . . . . . 13 |- {B} =/= (/)
12	8	elsnc 2492	. . . . . . . . . . . . . 14 |- ((/) e. {{B}} <-> (/) = {B})
13		eqcom 1520	. . . . . . . . . . . . . 14 |- ((/) = {B} <-> {B} = (/))
14	12, 13	bitri 171	. . . . . . . . . . . . 13 |- ((/) e. {{B}} <-> {B} = (/))
15	11, 14	nemtbir 1687	. . . . . . . . . . . 12 |- -. (/) e. {{B}}
16		nelneq2 1605	. . . . . . . . . . . 12 |- (((/) e. {{C}, (/)} /\ -. (/) e. {{B}}) -> -. {{C}, (/)} = {{B}})
17	9, 15, 16	mp2an 701	. . . . . . . . . . 11 |- -. {{C}, (/)} = {{B}}
18		eqcom 1520	. . . . . . . . . . 11 |- ({{C}, (/)} = {{B}} <-> {{B}} = {{C}, (/)})
19	17, 18	mtbi 189	. . . . . . . . . 10 |- -. {{B}} = {{C}, (/)}
20		biorf 740	. . . . . . . . . 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 198	. . . . . . . 8 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} = {{D}})
23		preq2 2510	. . . . . . . 8 |- ({{B}} = {{D}} -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
24	22, 23	syl 10	. . . . . . 7 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
25	1, 24	eqtr4d 1553	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
26		prex 2857	. . . . . . 7 |- {{A}, (/)} e. V
27		prex 2857	. . . . . . 7 |- {{C}, (/)} e. V
28	26, 27	preqr1 2546	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}} -> {{A}, (/)} = {{C}, (/)})
29	25, 28	syl 10	. . . . 5 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{A}, (/)} = {{C}, (/)})
30		snex 2826	. . . . . 6 |- {A} e. V
31		snex 2826	. . . . . 6 |- {C} e. V
32	30, 31	preqr1 2546	. . . . 5 |- ({{A}, (/)} = {{C}, (/)} -> {A} = {C})
33	29, 32	syl 10	. . . 4 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {A} = {C})
34		opthw.1	. . . . 5 |- A e. V
35	34	sneqr 2542	. . . 4 |- ({A} = {C} -> A = C)
36	33, 35	syl 10	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> A = C)
37		snex 2826	. . . . 5 |- {B} e. V
38	37	sneqr 2542	. . . 4 |- ({{B}} = {{D}} -> {B} = {D})
39	10	sneqr 2542	. . . 4 |- ({B} = {D} -> B = D)
40	22, 38, 39	3syl 20	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> B = D)
41	36, 40	jca 286	. 2 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> (A = C /\ B = D))
42		sneq 2475	. . . 4 |- (A = C -> {A} = {C})
43		preq1 2509	. . . 4 |- ({A} = {C} -> {{A}, (/)} = {{C}, (/)})
44		preq1 2509	. . . 4 |- ({{A}, (/)} = {{C}, (/)} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
45	42, 43, 44	3syl 20	. . 3 |- (A = C -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
46		sneq 2475	. . . 4 |- (B = D -> {B} = {D})
47		sneq 2475	. . . 4 |- ({B} = {D} -> {{B}} = {{D}})
48	46, 47, 23	3syl 20	. . 3 |- (B = D -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
49	45, 48	sylan9eq 1570	. 2 |- ((A = C /\ B = D) -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
50	41, 49	impbii 155	1 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))

Syntax hints:  -. wn 2   <-> wb 144   \/ wo 220   /\ wa 221   = wceq 992   e. wcel 994  Vcvv 1857  (/)c0 2332  {csn 2467  {cpr 2468

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471

Copyright terms: Public domain