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

Theorem opthhausdorff 5185
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 5041). 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 4388 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 5112 . . . 4 {𝐴, 𝑂} ∈ V
2 prex 5112 . . . 4 {𝐵, 𝑇} ∈ V
3 opthhausdorff.a . . . . . . 7 𝐴 ∈ V
4 opthhausdorff.1 . . . . . . 7 𝑂 ∈ V
53, 4pm3.2i 458 . . . . . 6 (𝐴 ∈ V ∧ 𝑂 ∈ V)
6 opthhausdorff.b . . . . . . 7 𝐵 ∈ V
7 opthhausdorff.2 . . . . . . 7 𝑇 ∈ V
86, 7pm3.2i 458 . . . . . 6 (𝐵 ∈ V ∧ 𝑇 ∈ V)
95, 8pm3.2i 458 . . . . 5 ((𝐴 ∈ V ∧ 𝑂 ∈ V) ∧ (𝐵 ∈ V ∧ 𝑇 ∈ V))
10 opthhausdorff.n . . . . . . . 8 𝐵𝑂
1110necomi 3043 . . . . . . 7 𝑂𝐵
12 opthhausdorff.3 . . . . . . 7 𝑂𝑇
1311, 12pm3.2i 458 . . . . . 6 (𝑂𝐵𝑂𝑇)
1413olci 884 . . . . 5 ((𝐴𝐵𝐴𝑇) ∨ (𝑂𝐵𝑂𝑇))
15 prneimg 4586 . . . . 5 (((𝐴 ∈ V ∧ 𝑂 ∈ V) ∧ (𝐵 ∈ V ∧ 𝑇 ∈ V)) → (((𝐴𝐵𝐴𝑇) ∨ (𝑂𝐵𝑂𝑇)) → {𝐴, 𝑂} ≠ {𝐵, 𝑇}))
169, 14, 15mp2 9 . . . 4 {𝐴, 𝑂} ≠ {𝐵, 𝑇}
17 preq12nebg 4596 . . . 4 (({𝐴, 𝑂} ∈ V ∧ {𝐵, 𝑇} ∈ V ∧ {𝐴, 𝑂} ≠ {𝐵, 𝑇}) → ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (({𝐴, 𝑂} = {𝐶, 𝑂} ∧ {𝐵, 𝑇} = {𝐷, 𝑇}) ∨ ({𝐴, 𝑂} = {𝐷, 𝑇} ∧ {𝐵, 𝑇} = {𝐶, 𝑂}))))
181, 2, 16, 17mp3an 1578 . . 3 ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (({𝐴, 𝑂} = {𝐶, 𝑂} ∧ {𝐵, 𝑇} = {𝐷, 𝑇}) ∨ ({𝐴, 𝑂} = {𝐷, 𝑇} ∧ {𝐵, 𝑇} = {𝐶, 𝑂})))
19 opthhausdorff.o . . . . . 6 𝐴𝑂
20 preq12nebg 4596 . . . . . 6 ((𝐴 ∈ V ∧ 𝑂 ∈ V ∧ 𝐴𝑂) → ({𝐴, 𝑂} = {𝐶, 𝑂} ↔ ((𝐴 = 𝐶𝑂 = 𝑂) ∨ (𝐴 = 𝑂𝑂 = 𝐶))))
213, 4, 19, 20mp3an 1578 . . . . 5 ({𝐴, 𝑂} = {𝐶, 𝑂} ↔ ((𝐴 = 𝐶𝑂 = 𝑂) ∨ (𝐴 = 𝑂𝑂 = 𝐶)))
22 opthhausdorff.t . . . . . 6 𝐵𝑇
23 preq12nebg 4596 . . . . . 6 ((𝐵 ∈ V ∧ 𝑇 ∈ V ∧ 𝐵𝑇) → ({𝐵, 𝑇} = {𝐷, 𝑇} ↔ ((𝐵 = 𝐷𝑇 = 𝑇) ∨ (𝐵 = 𝑇𝑇 = 𝐷))))
246, 7, 22, 23mp3an 1578 . . . . 5 ({𝐵, 𝑇} = {𝐷, 𝑇} ↔ ((𝐵 = 𝐷𝑇 = 𝑇) ∨ (𝐵 = 𝑇𝑇 = 𝐷)))
25 simpl 470 . . . . . . 7 ((𝐴 = 𝐶𝑂 = 𝑂) → 𝐴 = 𝐶)
26 simpl 470 . . . . . . 7 ((𝐵 = 𝐷𝑇 = 𝑇) → 𝐵 = 𝐷)
2725, 26anim12i 602 . . . . . 6 (((𝐴 = 𝐶𝑂 = 𝑂) ∧ (𝐵 = 𝐷𝑇 = 𝑇)) → (𝐴 = 𝐶𝐵 = 𝐷))
28 eqneqall 3000 . . . . . . . 8 (𝐴 = 𝑂 → (𝐴𝑂 → (𝐴 = 𝐶𝐵 = 𝐷)))
2919, 28mpi 20 . . . . . . 7 (𝐴 = 𝑂 → (𝐴 = 𝐶𝐵 = 𝐷))
3029adantr 468 . . . . . 6 ((𝐴 = 𝑂𝑂 = 𝐶) → (𝐴 = 𝐶𝐵 = 𝐷))
31 eqneqall 3000 . . . . . . . 8 (𝐵 = 𝑇 → (𝐵𝑇 → (𝐴 = 𝐶𝐵 = 𝐷)))
3222, 31mpi 20 . . . . . . 7 (𝐵 = 𝑇 → (𝐴 = 𝐶𝐵 = 𝐷))
3332adantr 468 . . . . . 6 ((𝐵 = 𝑇𝑇 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
3427, 30, 33ccase2 1053 . . . . 5 ((((𝐴 = 𝐶𝑂 = 𝑂) ∨ (𝐴 = 𝑂𝑂 = 𝐶)) ∧ ((𝐵 = 𝐷𝑇 = 𝑇) ∨ (𝐵 = 𝑇𝑇 = 𝐷))) → (𝐴 = 𝐶𝐵 = 𝐷))
3521, 24, 34syl2anb 587 . . . 4 (({𝐴, 𝑂} = {𝐶, 𝑂} ∧ {𝐵, 𝑇} = {𝐷, 𝑇}) → (𝐴 = 𝐶𝐵 = 𝐷))
36 preq12nebg 4596 . . . . . 6 ((𝐴 ∈ V ∧ 𝑂 ∈ V ∧ 𝐴𝑂) → ({𝐴, 𝑂} = {𝐷, 𝑇} ↔ ((𝐴 = 𝐷𝑂 = 𝑇) ∨ (𝐴 = 𝑇𝑂 = 𝐷))))
373, 4, 19, 36mp3an 1578 . . . . 5 ({𝐴, 𝑂} = {𝐷, 𝑇} ↔ ((𝐴 = 𝐷𝑂 = 𝑇) ∨ (𝐴 = 𝑇𝑂 = 𝐷)))
38 preq12nebg 4596 . . . . . 6 ((𝐵 ∈ V ∧ 𝑇 ∈ V ∧ 𝐵𝑇) → ({𝐵, 𝑇} = {𝐶, 𝑂} ↔ ((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶))))
396, 7, 22, 38mp3an 1578 . . . . 5 ({𝐵, 𝑇} = {𝐶, 𝑂} ↔ ((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)))
40 eqneqall 3000 . . . . . . . . . 10 (𝑂 = 𝑇 → (𝑂𝑇 → (𝐴 = 𝐶𝐵 = 𝐷)))
4112, 40mpi 20 . . . . . . . . 9 (𝑂 = 𝑇 → (𝐴 = 𝐶𝐵 = 𝐷))
4241adantl 469 . . . . . . . 8 ((𝐴 = 𝐷𝑂 = 𝑇) → (𝐴 = 𝐶𝐵 = 𝐷))
4342a1d 25 . . . . . . 7 ((𝐴 = 𝐷𝑂 = 𝑇) → (((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)) → (𝐴 = 𝐶𝐵 = 𝐷)))
4412necomi 3043 . . . . . . . . . . . 12 𝑇𝑂
45 eqneqall 3000 . . . . . . . . . . . 12 (𝑇 = 𝑂 → (𝑇𝑂 → (𝐴 = 𝐶𝐵 = 𝐷)))
4644, 45mpi 20 . . . . . . . . . . 11 (𝑇 = 𝑂 → (𝐴 = 𝐶𝐵 = 𝐷))
4746adantl 469 . . . . . . . . . 10 ((𝐵 = 𝐶𝑇 = 𝑂) → (𝐴 = 𝐶𝐵 = 𝐷))
4847a1d 25 . . . . . . . . 9 ((𝐵 = 𝐶𝑇 = 𝑂) → ((𝐴 = 𝑇𝑂 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷)))
49 eqneqall 3000 . . . . . . . . . . . 12 (𝐵 = 𝑂 → (𝐵𝑂 → (𝐴 = 𝐶𝐵 = 𝐷)))
5010, 49mpi 20 . . . . . . . . . . 11 (𝐵 = 𝑂 → (𝐴 = 𝐶𝐵 = 𝐷))
5150adantr 468 . . . . . . . . . 10 ((𝐵 = 𝑂𝑇 = 𝐶) → (𝐴 = 𝐶𝐵 = 𝐷))
5251a1d 25 . . . . . . . . 9 ((𝐵 = 𝑂𝑇 = 𝐶) → ((𝐴 = 𝑇𝑂 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷)))
5348, 52jaoi 875 . . . . . . . 8 (((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)) → ((𝐴 = 𝑇𝑂 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷)))
5453com12 32 . . . . . . 7 ((𝐴 = 𝑇𝑂 = 𝐷) → (((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)) → (𝐴 = 𝐶𝐵 = 𝐷)))
5543, 54jaoi 875 . . . . . 6 (((𝐴 = 𝐷𝑂 = 𝑇) ∨ (𝐴 = 𝑇𝑂 = 𝐷)) → (((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶)) → (𝐴 = 𝐶𝐵 = 𝐷)))
5655imp 395 . . . . 5 ((((𝐴 = 𝐷𝑂 = 𝑇) ∨ (𝐴 = 𝑇𝑂 = 𝐷)) ∧ ((𝐵 = 𝐶𝑇 = 𝑂) ∨ (𝐵 = 𝑂𝑇 = 𝐶))) → (𝐴 = 𝐶𝐵 = 𝐷))
5737, 39, 56syl2anb 587 . . . 4 (({𝐴, 𝑂} = {𝐷, 𝑇} ∧ {𝐵, 𝑇} = {𝐶, 𝑂}) → (𝐴 = 𝐶𝐵 = 𝐷))
5835, 57jaoi 875 . . 3 ((({𝐴, 𝑂} = {𝐶, 𝑂} ∧ {𝐵, 𝑇} = {𝐷, 𝑇}) ∨ ({𝐴, 𝑂} = {𝐷, 𝑇} ∧ {𝐵, 𝑇} = {𝐶, 𝑂})) → (𝐴 = 𝐶𝐵 = 𝐷))
5918, 58sylbi 208 . 2 ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} → (𝐴 = 𝐶𝐵 = 𝐷))
60 preq1 4470 . . . 4 (𝐴 = 𝐶 → {𝐴, 𝑂} = {𝐶, 𝑂})
6160adantr 468 . . 3 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝑂} = {𝐶, 𝑂})
62 preq1 4470 . . . 4 (𝐵 = 𝐷 → {𝐵, 𝑇} = {𝐷, 𝑇})
6362adantl 469 . . 3 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐵, 𝑇} = {𝐷, 𝑇})
6461, 63preq12d 4478 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → {{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}})
6559, 64impbii 200 1 ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2157  wne 2989  Vcvv 3402  {cpr 4383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-v 3404  df-dif 3783  df-un 3785  df-nul 4128  df-sn 4382  df-pr 4384
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator