Metamath Proof Explorer

Theorem opthhausdorff0

Description: Justification theorem for the ordered pair definition of Felix Hausdorff in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), 1914, p. 32: <. A , B >._H = { { A , O } , { B , T } } . Hausdorff used 1 and 2 instead of O and T , but actually, any two different fixed sets will do (e.g., O = (/) and T = { (/) } , see 0nep0 ). Furthermore, Hausdorff demanded that O and T are both different from A as well as B , which is actually not necessary if all involved classes exist as sets (i.e. are not proper classes), in contrast to opthhausdorff . See df-op for other ordered pair definitions. (Contributed by AV, 12-Jun-2022)

Ref Expression
Hypotheses opthhausdorff0.a ⊢ A ∈ V
opthhausdorff0.b ⊢ B ∈ V
opthhausdorff0.c ⊢ C ∈ V
opthhausdorff0.d ⊢ D ∈ V
opthhausdorff0.1 ⊢ O ∈ V
opthhausdorff0.2 ⊢ T ∈ V
opthhausdorff0.3 ⊢ O ≠ T
Assertion opthhausdorff0 ⊢ A O B T = C O D T ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 opthhausdorff0.a ⊢ A ∈ V
2 opthhausdorff0.b ⊢ B ∈ V
3 opthhausdorff0.c ⊢ C ∈ V
4 opthhausdorff0.d ⊢ D ∈ V
5 opthhausdorff0.1 ⊢ O ∈ V
6 opthhausdorff0.2 ⊢ T ∈ V
7 opthhausdorff0.3 ⊢ O ≠ T
8 prex ⊢ A O ∈ V
9 prex ⊢ B T ∈ V
10 prex ⊢ C O ∈ V
11 prex ⊢ D T ∈ V
12 8 9 10 11 preq12b ⊢ A O B T = C O D T ↔ A O = C O ∧ B T = D T ∨ A O = D T ∧ B T = C O
13 1 3 preqr1 ⊢ A O = C O → A = C
14 2 4 preqr1 ⊢ B T = D T → B = D
15 13 14 anim12i ⊢ A O = C O ∧ B T = D T → A = C ∧ B = D
16 1 5 4 6 preq12b ⊢ A O = D T ↔ A = D ∧ O = T ∨ A = T ∧ O = D
17 eqneqall ⊢ O = T → O ≠ T → B T = C O → A = C ∧ B = D
18 7 17 mpi ⊢ O = T → B T = C O → A = C ∧ B = D
19 18 adantl ⊢ A = D ∧ O = T → B T = C O → A = C ∧ B = D
20 2 6 3 5 preq12b ⊢ B T = C O ↔ B = C ∧ T = O ∨ B = O ∧ T = C
21 eqneqall ⊢ O = T → O ≠ T → A = T ∧ O = D → A = C ∧ B = D
22 7 21 mpi ⊢ O = T → A = T ∧ O = D → A = C ∧ B = D
23 22 eqcoms ⊢ T = O → A = T ∧ O = D → A = C ∧ B = D
24 23 adantl ⊢ B = C ∧ T = O → A = T ∧ O = D → A = C ∧ B = D
25 simpl ⊢ A = T ∧ O = D → A = T
26 simpr ⊢ B = O ∧ T = C → T = C
27 25 26 sylan9eqr ⊢ B = O ∧ T = C ∧ A = T ∧ O = D → A = C
28 simpl ⊢ B = O ∧ T = C → B = O
29 simpr ⊢ A = T ∧ O = D → O = D
30 28 29 sylan9eq ⊢ B = O ∧ T = C ∧ A = T ∧ O = D → B = D
31 27 30 jca ⊢ B = O ∧ T = C ∧ A = T ∧ O = D → A = C ∧ B = D
32 31 ex ⊢ B = O ∧ T = C → A = T ∧ O = D → A = C ∧ B = D
33 24 32 jaoi ⊢ B = C ∧ T = O ∨ B = O ∧ T = C → A = T ∧ O = D → A = C ∧ B = D
34 20 33 sylbi ⊢ B T = C O → A = T ∧ O = D → A = C ∧ B = D
35 34 com12 ⊢ A = T ∧ O = D → B T = C O → A = C ∧ B = D
36 19 35 jaoi ⊢ A = D ∧ O = T ∨ A = T ∧ O = D → B T = C O → A = C ∧ B = D
37 16 36 sylbi ⊢ A O = D T → B T = C O → A = C ∧ B = D
38 37 imp ⊢ A O = D T ∧ B T = C O → A = C ∧ B = D
39 15 38 jaoi ⊢ A O = C O ∧ B T = D T ∨ A O = D T ∧ B T = C O → A = C ∧ B = D
40 12 39 sylbi ⊢ A O B T = C O D T → A = C ∧ B = D
41 preq1 ⊢ A = C → A O = C O
42 41 adantr ⊢ A = C ∧ B = D → A O = C O
43 preq1 ⊢ B = D → B T = D T
44 43 adantl ⊢ A = C ∧ B = D → B T = D T
45 42 44 preq12d ⊢ A = C ∧ B = D → A O B T = C O D T
46 40 45 impbii ⊢ A O B T = C O D T ↔ A = C ∧ B = D