Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  opthwiener Structured version   Visualization version   GIF version

Theorem opthwiener 5107
 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 4323 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.)
Hypotheses
Ref Expression
opthw.1 𝐴 ∈ V
opthw.2 𝐵 ∈ V
Assertion
Ref Expression
opthwiener ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} ↔ (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem opthwiener
StepHypRef Expression
1 id 22 . . . . . . 7 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}})
2 snex 5036 . . . . . . . . . . . 12 {{𝐵}} ∈ V
32prid2 4434 . . . . . . . . . . 11 {{𝐵}} ∈ {{{𝐴}, ∅}, {{𝐵}}}
4 eleq2 2839 . . . . . . . . . . 11 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → ({{𝐵}} ∈ {{{𝐴}, ∅}, {{𝐵}}} ↔ {{𝐵}} ∈ {{{𝐶}, ∅}, {{𝐷}}}))
53, 4mpbii 223 . . . . . . . . . 10 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{𝐵}} ∈ {{{𝐶}, ∅}, {{𝐷}}})
62elpr 4338 . . . . . . . . . 10 ({{𝐵}} ∈ {{{𝐶}, ∅}, {{𝐷}}} ↔ ({{𝐵}} = {{𝐶}, ∅} ∨ {{𝐵}} = {{𝐷}}))
75, 6sylib 208 . . . . . . . . 9 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → ({{𝐵}} = {{𝐶}, ∅} ∨ {{𝐵}} = {{𝐷}}))
8 0ex 4924 . . . . . . . . . . . . 13 ∅ ∈ V
98prid2 4434 . . . . . . . . . . . 12 ∅ ∈ {{𝐶}, ∅}
10 opthw.2 . . . . . . . . . . . . . 14 𝐵 ∈ V
1110snnz 4444 . . . . . . . . . . . . 13 {𝐵} ≠ ∅
128elsn 4331 . . . . . . . . . . . . . 14 (∅ ∈ {{𝐵}} ↔ ∅ = {𝐵})
13 eqcom 2778 . . . . . . . . . . . . . 14 (∅ = {𝐵} ↔ {𝐵} = ∅)
1412, 13bitri 264 . . . . . . . . . . . . 13 (∅ ∈ {{𝐵}} ↔ {𝐵} = ∅)
1511, 14nemtbir 3038 . . . . . . . . . . . 12 ¬ ∅ ∈ {{𝐵}}
16 nelneq2 2875 . . . . . . . . . . . 12 ((∅ ∈ {{𝐶}, ∅} ∧ ¬ ∅ ∈ {{𝐵}}) → ¬ {{𝐶}, ∅} = {{𝐵}})
179, 15, 16mp2an 672 . . . . . . . . . . 11 ¬ {{𝐶}, ∅} = {{𝐵}}
18 eqcom 2778 . . . . . . . . . . 11 ({{𝐶}, ∅} = {{𝐵}} ↔ {{𝐵}} = {{𝐶}, ∅})
1917, 18mtbi 311 . . . . . . . . . 10 ¬ {{𝐵}} = {{𝐶}, ∅}
20 biorf 920 . . . . . . . . . 10 (¬ {{𝐵}} = {{𝐶}, ∅} → ({{𝐵}} = {{𝐷}} ↔ ({{𝐵}} = {{𝐶}, ∅} ∨ {{𝐵}} = {{𝐷}})))
2119, 20ax-mp 5 . . . . . . . . 9 ({{𝐵}} = {{𝐷}} ↔ ({{𝐵}} = {{𝐶}, ∅} ∨ {{𝐵}} = {{𝐷}}))
227, 21sylibr 224 . . . . . . . 8 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{𝐵}} = {{𝐷}})
2322preq2d 4411 . . . . . . 7 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{{𝐶}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}})
241, 23eqtr4d 2808 . . . . . 6 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐵}}})
25 prex 5037 . . . . . . 7 {{𝐴}, ∅} ∈ V
26 prex 5037 . . . . . . 7 {{𝐶}, ∅} ∈ V
2725, 26preqr1 4511 . . . . . 6 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐵}}} → {{𝐴}, ∅} = {{𝐶}, ∅})
2824, 27syl 17 . . . . 5 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{𝐴}, ∅} = {{𝐶}, ∅})
29 snex 5036 . . . . . 6 {𝐴} ∈ V
30 snex 5036 . . . . . 6 {𝐶} ∈ V
3129, 30preqr1 4511 . . . . 5 ({{𝐴}, ∅} = {{𝐶}, ∅} → {𝐴} = {𝐶})
3228, 31syl 17 . . . 4 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {𝐴} = {𝐶})
33 opthw.1 . . . . 5 𝐴 ∈ V
3433sneqr 4504 . . . 4 ({𝐴} = {𝐶} → 𝐴 = 𝐶)
3532, 34syl 17 . . 3 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → 𝐴 = 𝐶)
36 snex 5036 . . . . . 6 {𝐵} ∈ V
3736sneqr 4504 . . . . 5 ({{𝐵}} = {{𝐷}} → {𝐵} = {𝐷})
3822, 37syl 17 . . . 4 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {𝐵} = {𝐷})
3910sneqr 4504 . . . 4 ({𝐵} = {𝐷} → 𝐵 = 𝐷)
4038, 39syl 17 . . 3 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → 𝐵 = 𝐷)
4135, 40jca 501 . 2 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → (𝐴 = 𝐶𝐵 = 𝐷))
42 sneq 4326 . . . . 5 (𝐴 = 𝐶 → {𝐴} = {𝐶})
4342preq1d 4410 . . . 4 (𝐴 = 𝐶 → {{𝐴}, ∅} = {{𝐶}, ∅})
4443preq1d 4410 . . 3 (𝐴 = 𝐶 → {{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐵}}})
45 sneq 4326 . . . . 5 (𝐵 = 𝐷 → {𝐵} = {𝐷})
46 sneq 4326 . . . . 5 ({𝐵} = {𝐷} → {{𝐵}} = {{𝐷}})
4745, 46syl 17 . . . 4 (𝐵 = 𝐷 → {{𝐵}} = {{𝐷}})
4847preq2d 4411 . . 3 (𝐵 = 𝐷 → {{{𝐶}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}})
4944, 48sylan9eq 2825 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → {{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}})
5041, 49impbii 199 1 ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} ↔ (𝐴 = 𝐶𝐵 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 382   ∨ wo 834   = wceq 1631   ∈ wcel 2145  Vcvv 3351  ∅c0 4063  {csn 4316  {cpr 4318 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-v 3353  df-dif 3726  df-un 3728  df-nul 4064  df-sn 4317  df-pr 4319 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator