This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opthhausdorff

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 in full extent ( A =/= T is not required). This definition is meaningful only for classes A and B that exist as sets (i.e., are not proper classes): If A and C were different proper classes ( A =/= C ), then { { A , O } , { B , T } } = { { C , O } , { D , T } <-> { { O } , { B , T } } = { { O } , { D , T } is true if B = D , but ( A = C /\ B = D ) would be false. See df-op for other ordered pair definitions. (Contributed by AV, 14-Jun-2022)

Ref Expression
Hypotheses opthhausdorff.a ⊢ A ∈ V
opthhausdorff.b ⊢ B ∈ V
opthhausdorff.o ⊢ A ≠ O
opthhausdorff.n ⊢ B ≠ O
opthhausdorff.t ⊢ B ≠ T
opthhausdorff.1 ⊢ O ∈ V
opthhausdorff.2 ⊢ T ∈ V
opthhausdorff.3 ⊢ O ≠ T
Assertion opthhausdorff ⊢ A O B T = C O D T ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 opthhausdorff.a ⊢ A ∈ V
2 opthhausdorff.b ⊢ B ∈ V
3 opthhausdorff.o ⊢ A ≠ O
4 opthhausdorff.n ⊢ B ≠ O
5 opthhausdorff.t ⊢ B ≠ T
6 opthhausdorff.1 ⊢ O ∈ V
7 opthhausdorff.2 ⊢ T ∈ V
8 opthhausdorff.3 ⊢ O ≠ T
9 prex ⊢ A O ∈ V
10 prex ⊢ B T ∈ V
11 1 6 pm3.2i ⊢ A ∈ V ∧ O ∈ V
12 2 7 pm3.2i ⊢ B ∈ V ∧ T ∈ V
13 11 12 pm3.2i ⊢ A ∈ V ∧ O ∈ V ∧ B ∈ V ∧ T ∈ V
14 4 necomi ⊢ O ≠ B
15 14 8 pm3.2i ⊢ O ≠ B ∧ O ≠ T
16 15 olci ⊢ A ≠ B ∧ A ≠ T ∨ O ≠ B ∧ O ≠ T
17 prneimg ⊢ A ∈ V ∧ O ∈ V ∧ B ∈ V ∧ T ∈ V → A ≠ B ∧ A ≠ T ∨ O ≠ B ∧ O ≠ T → A O ≠ B T
18 13 16 17 mp2 ⊢ A O ≠ B T
19 preq12nebg ⊢ A O ∈ V ∧ B T ∈ V ∧ A O ≠ B T → A O B T = C O D T ↔ A O = C O ∧ B T = D T ∨ A O = D T ∧ B T = C O
20 9 10 18 19 mp3an ⊢ A O B T = C O D T ↔ A O = C O ∧ B T = D T ∨ A O = D T ∧ B T = C O
21 preq12nebg ⊢ A ∈ V ∧ O ∈ V ∧ A ≠ O → A O = C O ↔ A = C ∧ O = O ∨ A = O ∧ O = C
22 1 6 3 21 mp3an ⊢ A O = C O ↔ A = C ∧ O = O ∨ A = O ∧ O = C
23 preq12nebg ⊢ B ∈ V ∧ T ∈ V ∧ B ≠ T → B T = D T ↔ B = D ∧ T = T ∨ B = T ∧ T = D
24 2 7 5 23 mp3an ⊢ B T = D T ↔ B = D ∧ T = T ∨ B = T ∧ T = D
25 simpl ⊢ A = C ∧ O = O → A = C
26 simpl ⊢ B = D ∧ T = T → B = D
27 25 26 anim12i ⊢ A = C ∧ O = O ∧ B = D ∧ T = T → A = C ∧ B = D
28 eqneqall ⊢ A = O → A ≠ O → A = C ∧ B = D
29 3 28 mpi ⊢ A = O → A = C ∧ B = D
30 29 adantr ⊢ A = O ∧ O = C → A = C ∧ B = D
31 eqneqall ⊢ B = T → B ≠ T → A = C ∧ B = D
32 5 31 mpi ⊢ B = T → A = C ∧ B = D
33 32 adantr ⊢ B = T ∧ T = D → A = C ∧ B = D
34 27 30 33 ccase2 ⊢ A = C ∧ O = O ∨ A = O ∧ O = C ∧ B = D ∧ T = T ∨ B = T ∧ T = D → A = C ∧ B = D
35 22 24 34 syl2anb ⊢ A O = C O ∧ B T = D T → A = C ∧ B = D
36 preq12nebg ⊢ A ∈ V ∧ O ∈ V ∧ A ≠ O → A O = D T ↔ A = D ∧ O = T ∨ A = T ∧ O = D
37 1 6 3 36 mp3an ⊢ A O = D T ↔ A = D ∧ O = T ∨ A = T ∧ O = D
38 preq12nebg ⊢ B ∈ V ∧ T ∈ V ∧ B ≠ T → B T = C O ↔ B = C ∧ T = O ∨ B = O ∧ T = C
39 2 7 5 38 mp3an ⊢ B T = C O ↔ B = C ∧ T = O ∨ B = O ∧ T = C
40 eqneqall ⊢ O = T → O ≠ T → A = C ∧ B = D
41 8 40 mpi ⊢ O = T → A = C ∧ B = D
42 41 adantl ⊢ A = D ∧ O = T → A = C ∧ B = D
43 42 a1d ⊢ A = D ∧ O = T → B = C ∧ T = O ∨ B = O ∧ T = C → A = C ∧ B = D
44 8 necomi ⊢ T ≠ O
45 eqneqall ⊢ T = O → T ≠ O → A = C ∧ B = D
46 44 45 mpi ⊢ T = O → A = C ∧ B = D
47 46 adantl ⊢ B = C ∧ T = O → A = C ∧ B = D
48 47 a1d ⊢ B = C ∧ T = O → A = T ∧ O = D → A = C ∧ B = D
49 eqneqall ⊢ B = O → B ≠ O → A = C ∧ B = D
50 4 49 mpi ⊢ B = O → A = C ∧ B = D
51 50 adantr ⊢ B = O ∧ T = C → A = C ∧ B = D
52 51 a1d ⊢ B = O ∧ T = C → A = T ∧ O = D → A = C ∧ B = D
53 48 52 jaoi ⊢ B = C ∧ T = O ∨ B = O ∧ T = C → A = T ∧ O = D → A = C ∧ B = D
54 53 com12 ⊢ A = T ∧ O = D → B = C ∧ T = O ∨ B = O ∧ T = C → A = C ∧ B = D
55 43 54 jaoi ⊢ A = D ∧ O = T ∨ A = T ∧ O = D → B = C ∧ T = O ∨ B = O ∧ T = C → A = C ∧ B = D
56 55 imp ⊢ A = D ∧ O = T ∨ A = T ∧ O = D ∧ B = C ∧ T = O ∨ B = O ∧ T = C → A = C ∧ B = D
57 37 39 56 syl2anb ⊢ A O = D T ∧ B T = C O → A = C ∧ B = D
58 35 57 jaoi ⊢ A O = C O ∧ B T = D T ∨ A O = D T ∧ B T = C O → A = C ∧ B = D
59 20 58 sylbi ⊢ A O B T = C O D T → A = C ∧ B = D
60 preq1 ⊢ A = C → A O = C O
61 60 adantr ⊢ A = C ∧ B = D → A O = C O
62 preq1 ⊢ B = D → B T = D T
63 62 adantl ⊢ A = C ∧ B = D → B T = D T
64 61 63 preq12d ⊢ A = C ∧ B = D → A O B T = C O D T
65 59 64 impbii ⊢ A O B T = C O D T ↔ A = C ∧ B = D