Theorem opthwiener 2802

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 2412 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 2745	. . . . . . . . . . . 12 |- {{B}} e. V
3	2	pri2 2447	. . . . . . . . . . 11 |- {{B}} e. {{{A}, (/)}, {{B}}}
4		eleq2 1532	. . . . . . . . . . 11 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} e. {{{A}, (/)}, {{B}}} <-> {{B}} e. {{{C}, (/)}, {{D}}}))
5	3, 4	mpbii 193	. . . . . . . . . 10 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} e. {{{C}, (/)}, {{D}}})
6	2	elpr 2420	. . . . . . . . . 10 |- ({{B}} e. {{{C}, (/)}, {{D}}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
7	5, 6	sylib 198	. . . . . . . . 9 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
8		0ex 2706	. . . . . . . . . . . . 13 |- (/) e. V
9	8	pri2 2447	. . . . . . . . . . . 12 |- (/) e. {{C}, (/)}
10		opthw.2	. . . . . . . . . . . . . 14 |- B e. V
11	10	snnz 2454	. . . . . . . . . . . . 13 |- {B} =/= (/)
12	8	elsnc 2427	. . . . . . . . . . . . . 14 |- ((/) e. {{B}} <-> (/) = {B})
13		eqcom 1474	. . . . . . . . . . . . . 14 |- ((/) = {B} <-> {B} = (/))
14	12, 13	bitr 173	. . . . . . . . . . . . 13 |- ((/) e. {{B}} <-> {B} = (/))
15	11, 14	nemtbir 1638	. . . . . . . . . . . 12 |- -. (/) e. {{B}}
16		nelneq2 1559	. . . . . . . . . . . 12 |- (((/) e. {{C}, (/)} /\ -. (/) e. {{B}}) -> -. {{C}, (/)} = {{B}})
17	9, 15, 16	mp2an 696	. . . . . . . . . . 11 |- -. {{C}, (/)} = {{B}}
18		eqcom 1474	. . . . . . . . . . 11 |- ({{C}, (/)} = {{B}} <-> {{B}} = {{C}, (/)})
19	17, 18	mtbi 191	. . . . . . . . . 10 |- -. {{B}} = {{C}, (/)}
20		biorf 734	. . . . . . . . . 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 200	. . . . . . . 8 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} = {{D}})
23		preq2 2445	. . . . . . . 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 1507	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
26		prex 2776	. . . . . . 7 |- {{A}, (/)} e. V
27		prex 2776	. . . . . . 7 |- {{C}, (/)} e. V
28	26, 27	preqr1 2477	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}} -> {{A}, (/)} = {{C}, (/)})
29	25, 28	syl 10	. . . . 5 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{A}, (/)} = {{C}, (/)})
30		snex 2745	. . . . . 6 |- {A} e. V
31		snex 2745	. . . . . 6 |- {C} e. V
32	30, 31	preqr1 2477	. . . . 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 2473	. . . 4 |- ({A} = {C} -> A = C)
36	33, 35	syl 10	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> A = C)
37		snex 2745	. . . . 5 |- {B} e. V
38	37	sneqr 2473	. . . 4 |- ({{B}} = {{D}} -> {B} = {D})
39	10	sneqr 2473	. . . 4 |- ({B} = {D} -> B = D)
40	22, 38, 39	3syl 20	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> B = D)
41	36, 40	jca 288	. 2 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> (A = C /\ B = D))
42		sneq 2413	. . . 4 |- (A = C -> {A} = {C})
43		preq1 2444	. . . 4 |- ({A} = {C} -> {{A}, (/)} = {{C}, (/)})
44		preq1 2444	. . . 4 |- ({{A}, (/)} = {{C}, (/)} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
45	42, 43, 44	3syl 20	. . 3 |- (A = C -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
46		sneq 2413	. . . 4 |- (B = D -> {B} = {D})
47		sneq 2413	. . . 4 |- ({B} = {D} -> {{B}} = {{D}})
48	46, 47, 23	3syl 20	. . 3 |- (B = D -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
49	45, 48	sylan9eq 1524	. 2 |- ((A = C /\ B = D) -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
50	41, 49	impbi 157	1 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))

Syntax hints:  -. wn 2   <-> wb 146   \/ wo 222   /\ wa 223   = wceq 954   e. wcel 956  Vcvv 1807  (/)c0 2276  {csn 2405  {cpr 2406

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409

Copyright terms: Public domain