Theorem opthwiener 2863

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 2468 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 2806	. . . . . . . . . . . 12 |- {{B}} e. V
3	2	prid2 2505	. . . . . . . . . . 11 |- {{B}} e. {{{A}, (/)}, {{B}}}
4		eleq2 1582	. . . . . . . . . . 11 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} e. {{{A}, (/)}, {{B}}} <-> {{B}} e. {{{C}, (/)}, {{D}}}))
5	3, 4	mpbii 200	. . . . . . . . . 10 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} e. {{{C}, (/)}, {{D}}})
6	2	elpr 2476	. . . . . . . . . 10 |- ({{B}} e. {{{C}, (/)}, {{D}}} <-> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
7	5, 6	sylib 205	. . . . . . . . 9 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> ({{B}} = {{C}, (/)} \/ {{B}} = {{D}}))
8		0ex 2766	. . . . . . . . . . . . 13 |- (/) e. V
9	8	prid2 2505	. . . . . . . . . . . 12 |- (/) e. {{C}, (/)}
10		opthw.2	. . . . . . . . . . . . . 14 |- B e. V
11	10	snnz 2512	. . . . . . . . . . . . 13 |- {B} =/= (/)
12	8	elsnc 2483	. . . . . . . . . . . . . 14 |- ((/) e. {{B}} <-> (/) = {B})
13		eqcom 1524	. . . . . . . . . . . . . 14 |- ((/) = {B} <-> {B} = (/))
14	12, 13	bitri 180	. . . . . . . . . . . . 13 |- ((/) e. {{B}} <-> {B} = (/))
15	11, 14	nemtbir 1688	. . . . . . . . . . . 12 |- -. (/) e. {{B}}
16		nelneq2 1609	. . . . . . . . . . . 12 |- (((/) e. {{C}, (/)} /\ -. (/) e. {{B}}) -> -. {{C}, (/)} = {{B}})
17	9, 15, 16	mp2an 709	. . . . . . . . . . 11 |- -. {{C}, (/)} = {{B}}
18		eqcom 1524	. . . . . . . . . . 11 |- ({{C}, (/)} = {{B}} <-> {{B}} = {{C}, (/)})
19	17, 18	mtbi 198	. . . . . . . . . 10 |- -. {{B}} = {{C}, (/)}
20		biorf 747	. . . . . . . . . 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 207	. . . . . . . 8 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{B}} = {{D}})
23		preq2 2501	. . . . . . . 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 1557	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
26		prex 2837	. . . . . . 7 |- {{A}, (/)} e. V
27		prex 2837	. . . . . . 7 |- {{C}, (/)} e. V
28	26, 27	preqr1 2535	. . . . . 6 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}} -> {{A}, (/)} = {{C}, (/)})
29	25, 28	syl 10	. . . . 5 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> {{A}, (/)} = {{C}, (/)})
30		snex 2806	. . . . . 6 |- {A} e. V
31		snex 2806	. . . . . 6 |- {C} e. V
32	30, 31	preqr1 2535	. . . . 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 2531	. . . 4 |- ({A} = {C} -> A = C)
36	33, 35	syl 10	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> A = C)
37		snex 2806	. . . . 5 |- {B} e. V
38	37	sneqr 2531	. . . 4 |- ({{B}} = {{D}} -> {B} = {D})
39	10	sneqr 2531	. . . 4 |- ({B} = {D} -> B = D)
40	22, 38, 39	3syl 20	. . 3 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> B = D)
41	36, 40	jca 295	. 2 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} -> (A = C /\ B = D))
42		sneq 2469	. . . 4 |- (A = C -> {A} = {C})
43		preq1 2500	. . . 4 |- ({A} = {C} -> {{A}, (/)} = {{C}, (/)})
44		preq1 2500	. . . 4 |- ({{A}, (/)} = {{C}, (/)} -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
45	42, 43, 44	3syl 20	. . 3 |- (A = C -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{B}}})
46		sneq 2469	. . . 4 |- (B = D -> {B} = {D})
47		sneq 2469	. . . 4 |- ({B} = {D} -> {{B}} = {{D}})
48	46, 47, 23	3syl 20	. . 3 |- (B = D -> {{{C}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
49	45, 48	sylan9eq 1574	. 2 |- ((A = C /\ B = D) -> {{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}})
50	41, 49	impbii 164	1 |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))

Syntax hints:  -. wn 2   <-> wb 153   \/ wo 229   /\ wa 230   = wceq 997   e. wcel 999  Vcvv 1858  (/)c0 2331  {csn 2461  {cpr 2462

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465

Copyright terms: Public domain