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