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

Theorem opthhausdorff 5111
 Description: Justification theorem for the ordered pair definition of Felix Hausdorff in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), 1914, p. 32: ⟨𝐴, 𝐵⟩_H = {{𝐴, 𝑂}, {𝐵, 𝑇}}. Hausdorff used 1 and 2 instead of 𝑂 and 𝑇, but actually, any two different fixed sets will do (e.g., 𝑂 = ∅ and 𝑇 = {∅}, see 0nep0 4968). Furthermore, Hausdorff demanded that 𝑂 and 𝑇 are both different from 𝐴 as well as 𝐵, which is actually not necessary in full extent (𝐴 ≠ 𝑇 is not required). This definition is meaningful only for classes 𝐴 and 𝐵 that exist as sets (i.e. are not proper classes): If 𝐴 and 𝐶 were different proper classes (𝐴 ≠ 𝐶), then {{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇} ↔ {{𝑂}, {𝐵, 𝑇}} = {{𝑂}, {𝐷, 𝑇} is true if 𝐵 = 𝐷, but (𝐴 = 𝐶 ∧ 𝐵 = 𝐷) would be false. See df-op 4324 for other ordered pair definitions. (Contributed by AV, 14-Jun-2022.)
Hypotheses
Ref Expression
opthhausdorff.a 𝐴 ∈ V
opthhausdorff.b 𝐵 ∈ V
opthhausdorff.o 𝐴𝑂
opthhausdorff.n 𝐵𝑂
opthhausdorff.t 𝐵𝑇
opthhausdorff.1 𝑂 ∈ V
opthhausdorff.2 𝑇 ∈ V
opthhausdorff.3 𝑂𝑇
Assertion
Ref Expression
opthhausdorff ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem opthhausdorff
StepHypRef Expression
1 prex 5038 . . . 4 {𝐴, 𝑂} ∈ V
2 prex 5038 . . . 4 {𝐵, 𝑇} ∈ V
3 opthhausdorff.a . . . . . . 7 𝐴 ∈ V
4 opthhausdorff.1 . . . . . . 7 𝑂 ∈ V
53, 4pm3.2i 456 . . . . . 6 (𝐴 ∈ V ∧ 𝑂 ∈ V)
6 opthhausdorff.b . . . . . . 7 𝐵 ∈ V
7 opthhausdorff.2 . . . . . . 7 𝑇 ∈ V
86, 7pm3.2i 456 . . . . . 6 (𝐵 ∈ V ∧ 𝑇 ∈ V)
95, 8pm3.2i 456 . . . . 5 ((𝐴 ∈ V ∧ 𝑂 ∈ V) ∧ (𝐵 ∈ V ∧ 𝑇 ∈ V))
10 opthhausdorff.n . . . . . . . 8 𝐵𝑂
1110necomi 2997 . . . . . . 7 𝑂𝐵
12 opthhausdorff.3 . . . . . . 7 𝑂𝑇
1311, 12pm3.2i 456 . . . . . 6 (𝑂𝐵𝑂𝑇)
1413olci 855 . . . . 5 ((𝐴𝐵𝐴𝑇) ∨ (𝑂𝐵𝑂𝑇))
15 prneimg 4520 . . . . 5 (((𝐴 ∈ V ∧ 𝑂 ∈ V) ∧ (𝐵 ∈ V ∧ 𝑇 ∈ V)) → (((𝐴𝐵𝐴𝑇) ∨ (𝑂𝐵𝑂𝑇)) → {𝐴, 𝑂} ≠ {𝐵, 𝑇}))
169, 14, 15mp2 9 . . . 4 {𝐴, 𝑂} ≠ {𝐵, 𝑇}
17 preq12nebg 4530 . . . 4 (({𝐴, 𝑂} ∈ V ∧ {𝐵, 𝑇} ∈ V ∧ {𝐴, 𝑂} ≠ {𝐵, 𝑇}) → ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (({𝐴, 𝑂} = {𝐶, 𝑂} ∧ {𝐵, 𝑇} = {𝐷, 𝑇}) ∨ ({𝐴, 𝑂} = {𝐷, 𝑇} ∧ {𝐵, 𝑇} = {𝐶, 𝑂}))))
181, 2, 16, 17mp3an 1572 . . 3 ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (({𝐴, 𝑂} = {𝐶, 𝑂} ∧ {𝐵, 𝑇} = {𝐷, 𝑇}) ∨ ({𝐴, 𝑂} = {𝐷, 𝑇} ∧ {𝐵, 𝑇} = {𝐶, 𝑂})))
19 opthhausdorff.o . . . . . 6 𝐴𝑂
20 preq12nebg 4530 . . . . . 6 ((𝐴 ∈ V ∧ 𝑂 ∈ V ∧ 𝐴𝑂) → ({𝐴, 𝑂} = {𝐶, 𝑂} ↔ ((𝐴 = 𝐶𝑂 = 𝑂) ∨ (𝐴 = 𝑂𝑂 = 𝐶))))
213, 4, 19, 20mp3an 1572 . . . . 5 ({𝐴, 𝑂} = {𝐶, 𝑂} ↔ ((𝐴 = 𝐶𝑂 = 𝑂) ∨ (𝐴 = 𝑂𝑂 = 𝐶)))
22 opthhausdorff.t . . . . . 6 𝐵𝑇
23 preq12nebg 4530 . . . . . 6 ((𝐵 ∈ V ∧ 𝑇 ∈ V ∧ 𝐵𝑇) → ({𝐵, 𝑇} = {𝐷, 𝑇} ↔ ((𝐵 = 𝐷𝑇 = 𝑇) ∨ (𝐵 = 𝑇𝑇 = 𝐷))))
246, 7, 22, 23mp3an 1572 . . . . 5 ({𝐵, 𝑇} = {𝐷, 𝑇} ↔ ((𝐵 = 𝐷𝑇 = 𝑇) ∨ (𝐵 = 𝑇𝑇 = 𝐷)))
25 simpl 468 . . . . . . 7 ((𝐴 = 𝐶𝑂 = 𝑂) → 𝐴 = 𝐶)
26 simpl 468 . . . . . . 7 ((𝐵 = 𝐷𝑇 = 𝑇) → 𝐵 = 𝐷)
2725, 26anim12i 600 . . . . . 6 (((𝐴 = 𝐶𝑂 = 𝑂) ∧ (𝐵 = 𝐷𝑇 = 𝑇)) → (𝐴 = 𝐶𝐵 = 𝐷))
28 eqneqall 2954 . . . . . . . 8 (𝐴 = 𝑂 → (𝐴𝑂 → (𝐴 = 𝐶𝐵 = 𝐷)))
2919, 28mpi 20 . . . . . . 7 (𝐴 = 𝑂 → (𝐴 = 𝐶𝐵 = 𝐷))
3029adantr 466 . . . . . 6 ((𝐴 = 𝑂𝑂 = 𝐶) → (𝐴 = 𝐶𝐵 = 𝐷))
31 eqneqall 2954 . . . . . . . 8 (𝐵 = 𝑇 → (𝐵𝑇 → (𝐴 = 𝐶𝐵 = 𝐷)))
3222, 31mpi 20 . . . . . . 7 (𝐵 = 𝑇 → (𝐴 = 𝐶𝐵 = 𝐷))
3332adantr 466 . . . . . 6 ((𝐵 = 𝑇𝑇 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
3427, 30, 33ccase2 1024 . . . . 5 ((((𝐴 = 𝐶𝑂 = 𝑂) ∨ (𝐴 = 𝑂𝑂 = 𝐶)) ∧ ((𝐵 = 𝐷𝑇 = 𝑇) ∨ (𝐵 = 𝑇𝑇 = 𝐷))) → (𝐴 = 𝐶𝐵 = 𝐷))
3521, 24, 34syl2anb 585 . . . 4 (({𝐴, 𝑂} = {𝐶, 𝑂} ∧ {𝐵, 𝑇} = {𝐷, 𝑇}) → (𝐴 = 𝐶𝐵 = 𝐷))
36 preq12nebg 4530 . . . . . 6 ((𝐴 ∈ V ∧ 𝑂 ∈ V ∧ 𝐴𝑂) → ({𝐴, 𝑂} = {𝐷, 𝑇} ↔ ((𝐴 = 𝐷𝑂 = 𝑇) ∨ (𝐴 = 𝑇𝑂 = 𝐷))))
373, 4, 19, 36mp3an 1572 . . . . 5 ({𝐴, 𝑂} = {𝐷, 𝑇} ↔ ((𝐴 = 𝐷𝑂 = 𝑇) ∨ (𝐴 = 𝑇𝑂 = 𝐷)))
38 preq12nebg 4530 . . . . . 6 ((𝐵 ∈ V ∧ 𝑇 ∈ V ∧ 𝐵𝑇) → ({𝐵, 𝑇} = {𝐶, 𝑂} ↔ ((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶))))
396, 7, 22, 38mp3an 1572 . . . . 5 ({𝐵, 𝑇} = {𝐶, 𝑂} ↔ ((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)))
40 eqneqall 2954 . . . . . . . . . 10 (𝑂 = 𝑇 → (𝑂𝑇 → (𝐴 = 𝐶𝐵 = 𝐷)))
4112, 40mpi 20 . . . . . . . . 9 (𝑂 = 𝑇 → (𝐴 = 𝐶𝐵 = 𝐷))
4241adantl 467 . . . . . . . 8 ((𝐴 = 𝐷𝑂 = 𝑇) → (𝐴 = 𝐶𝐵 = 𝐷))
4342a1d 25 . . . . . . 7 ((𝐴 = 𝐷𝑂 = 𝑇) → (((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)) → (𝐴 = 𝐶𝐵 = 𝐷)))
4412necomi 2997 . . . . . . . . . . . 12 𝑇𝑂
45 eqneqall 2954 . . . . . . . . . . . 12 (𝑇 = 𝑂 → (𝑇𝑂 → (𝐴 = 𝐶𝐵 = 𝐷)))
4644, 45mpi 20 . . . . . . . . . . 11 (𝑇 = 𝑂 → (𝐴 = 𝐶𝐵 = 𝐷))
4746adantl 467 . . . . . . . . . 10 ((𝐵 = 𝐶𝑇 = 𝑂) → (𝐴 = 𝐶𝐵 = 𝐷))
4847a1d 25 . . . . . . . . 9 ((𝐵 = 𝐶𝑇 = 𝑂) → ((𝐴 = 𝑇𝑂 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷)))
49 eqneqall 2954 . . . . . . . . . . . 12 (𝐵 = 𝑂 → (𝐵𝑂 → (𝐴 = 𝐶𝐵 = 𝐷)))
5010, 49mpi 20 . . . . . . . . . . 11 (𝐵 = 𝑂 → (𝐴 = 𝐶𝐵 = 𝐷))
5150adantr 466 . . . . . . . . . 10 ((𝐵 = 𝑂𝑇 = 𝐶) → (𝐴 = 𝐶𝐵 = 𝐷))
5251a1d 25 . . . . . . . . 9 ((𝐵 = 𝑂𝑇 = 𝐶) → ((𝐴 = 𝑇𝑂 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷)))
5348, 52jaoi 846 . . . . . . . 8 (((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)) → ((𝐴 = 𝑇𝑂 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷)))
5453com12 32 . . . . . . 7 ((𝐴 = 𝑇𝑂 = 𝐷) → (((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)) → (𝐴 = 𝐶𝐵 = 𝐷)))
5543, 54jaoi 846 . . . . . 6 (((𝐴 = 𝐷𝑂 = 𝑇) ∨ (𝐴 = 𝑇𝑂 = 𝐷)) → (((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)) → (𝐴 = 𝐶𝐵 = 𝐷)))
5655imp 393 . . . . 5 ((((𝐴 = 𝐷𝑂 = 𝑇) ∨ (𝐴 = 𝑇𝑂 = 𝐷)) ∧ ((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶))) → (𝐴 = 𝐶𝐵 = 𝐷))
5737, 39, 56syl2anb 585 . . . 4 (({𝐴, 𝑂} = {𝐷, 𝑇} ∧ {𝐵, 𝑇} = {𝐶, 𝑂}) → (𝐴 = 𝐶𝐵 = 𝐷))
5835, 57jaoi 846 . . 3 ((({𝐴, 𝑂} = {𝐶, 𝑂} ∧ {𝐵, 𝑇} = {𝐷, 𝑇}) ∨ ({𝐴, 𝑂} = {𝐷, 𝑇} ∧ {𝐵, 𝑇} = {𝐶, 𝑂})) → (𝐴 = 𝐶𝐵 = 𝐷))
5918, 58sylbi 207 . 2 ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} → (𝐴 = 𝐶𝐵 = 𝐷))
60 preq1 4405 . . . 4 (𝐴 = 𝐶 → {𝐴, 𝑂} = {𝐶, 𝑂})
6160adantr 466 . . 3 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝑂} = {𝐶, 𝑂})
62 preq1 4405 . . . 4 (𝐵 = 𝐷 → {𝐵, 𝑇} = {𝐷, 𝑇})
6362adantl 467 . . 3 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐵, 𝑇} = {𝐷, 𝑇})
6461, 63preq12d 4413 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → {{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}})
6559, 64impbii 199 1 ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶𝐵 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∨ wo 836   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  Vcvv 3351  {cpr 4319 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 4916  ax-nul 4924  ax-pr 5035 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  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 4318  df-pr 4320 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator