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 ∈ V
opthw.2	⊢ B ∈ 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}} ∈ V
3	2	pri2 1842	. . . . . . . . . . 11 ⊢ {{B}} ∈ {{{A}, ∅}, {{B}}}
4		eleq2 1150	. . . . . . . . . . 11 ⊢ ({{{A}, ∅}, {{B}}} = {{{C}, ∅}, {{D}}} → ({{B}} ∈ {{{A}, ∅}, {{B}}} ↔ {{B}} ∈ {{{C}, ∅}, {{D}}}))
5	3, 4	mpbii 168	. . . . . . . . . 10 ⊢ ({{{A}, ∅}, {{B}}} = {{{C}, ∅}, {{D}}} → {{B}} ∈ {{{C}, ∅}, {{D}}})
6	2	elpr 1823	. . . . . . . . . 10 ⊢ ({{B}} ∈ {{{C}, ∅}, {{D}}} ↔ ({{B}} = {{C}, ∅} ∨ {{B}} = {{D}}))
7	5, 6	sylib 173	. . . . . . . . 9 ⊢ ({{{A}, ∅}, {{B}}} = {{{C}, ∅}, {{D}}} → ({{B}} = {{C}, ∅} ∨ {{B}} = {{D}}))
8		0ex 1745	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
9	8	pri2 1842	. . . . . . . . . . . 12 ⊢ ∅ ∈ {{C}, ∅}
10		opthw.2	. . . . . . . . . . . . . 14 ⊢ B ∈ V
11	10	snnz 1846	. . . . . . . . . . . . 13 ⊢ ¬ {B} = ∅
12	8	elsnc 1826	. . . . . . . . . . . . . 14 ⊢ (∅ ∈ {{B}} ↔ ∅ = {B})
13		cleqcom 1103	. . . . . . . . . . . . . 14 ⊢ (∅ = {B} ↔ {B} = ∅)
14	12, 13	bitr 151	. . . . . . . . . . . . 13 ⊢ (∅ ∈ {{B}} ↔ {B} = ∅)
15	11, 14	mtbir 167	. . . . . . . . . . . 12 ⊢ ¬ ∅ ∈ {{B}}
16		clneq2 1169	. . . . . . . . . . . 12 ⊢ ((∅ ∈ {{C}, ∅} ∧ ¬ ∅ ∈ {{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}, ∅} ∈ V
27		prex 1892	. . . . . . 7 ⊢ {{C}, ∅} ∈ 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} ∈ V
31		snex 1859	. . . . . 6 ⊢ {C} ∈ 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 ∈ 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} ∈ 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   ∈ 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