Metamath Proof Explorer

Theorem opthwiener

Description: Justification theorem for the ordered pair definition in Norbert Wiener, A simplification of the logic of relations, Proceedings of the Cambridge Philosophical Society, 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 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003)

Ref Expression
Hypotheses opthw.1 ⊢A∈V
opthw.2 ⊢B∈V
Assertion opthwiener ⊢A∅B=C∅D↔A=C∧B=D

Proof

Step Hyp Ref Expression
1 opthw.1 ⊢A∈V
2 opthw.2 ⊢B∈V
3 id ⊢A∅B=C∅D→A∅B=C∅D
4 snex ⊢B∈V
5 4 prid2 ⊢B∈A∅B
6 eleq2 ⊢A∅B=C∅D→B∈A∅B↔B∈C∅D
7 5 6 mpbii ⊢A∅B=C∅D→B∈C∅D
8 4 elpr ⊢B∈C∅D↔B=C∅∨B=D
9 7 8 sylib ⊢A∅B=C∅D→B=C∅∨B=D
10 0ex ⊢∅∈V
11 10 prid2 ⊢∅∈C∅
12 2 snnz ⊢B≠∅
13 10 elsn ⊢∅∈B↔∅=B
14 eqcom ⊢∅=B↔B=∅
15 13 14 bitri ⊢∅∈B↔B=∅
16 12 15 nemtbir ⊢¬∅∈B
17 nelneq2 ⊢∅∈C∅∧¬∅∈B→¬C∅=B
18 11 16 17 mp2an ⊢¬C∅=B
19 eqcom ⊢C∅=B↔B=C∅
20 18 19 mtbi ⊢¬B=C∅
21 biorf ⊢¬B=C∅→B=D↔B=C∅∨B=D
22 20 21 ax-mp ⊢B=D↔B=C∅∨B=D
23 9 22 sylibr ⊢A∅B=C∅D→B=D
24 23 preq2d ⊢A∅B=C∅D→C∅B=C∅D
25 3 24 eqtr4d ⊢A∅B=C∅D→A∅B=C∅B
26 prex ⊢A∅∈V
27 prex ⊢C∅∈V
28 26 27 preqr1 ⊢A∅B=C∅B→A∅=C∅
29 25 28 syl ⊢A∅B=C∅D→A∅=C∅
30 snex ⊢A∈V
31 snex ⊢C∈V
32 30 31 preqr1 ⊢A∅=C∅→A=C
33 29 32 syl ⊢A∅B=C∅D→A=C
34 1 sneqr ⊢A=C→A=C
35 33 34 syl ⊢A∅B=C∅D→A=C
36 snex ⊢B∈V
37 36 sneqr ⊢B=D→B=D
38 23 37 syl ⊢A∅B=C∅D→B=D
39 2 sneqr ⊢B=D→B=D
40 38 39 syl ⊢A∅B=C∅D→B=D
41 35 40 jca ⊢A∅B=C∅D→A=C∧B=D
42 sneq ⊢A=C→A=C
43 42 preq1d ⊢A=C→A∅=C∅
44 43 preq1d ⊢A=C→A∅B=C∅B
45 sneq ⊢B=D→B=D
46 sneq ⊢B=D→B=D
47 45 46 syl ⊢B=D→B=D
48 47 preq2d ⊢B=D→C∅B=C∅D
49 44 48 sylan9eq ⊢A=C∧B=D→A∅B=C∅D
50 41 49 impbii ⊢A∅B=C∅D↔A=C∧B=D