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 ⊢ 𝐴 ∈ V
opthhausdorff.b ⊢ 𝐵 ∈ V
opthhausdorff.o ⊢ 𝐴 ≠ 𝑂
opthhausdorff.n ⊢ 𝐵 ≠ 𝑂
opthhausdorff.t ⊢ 𝐵 ≠ 𝑇
opthhausdorff.1 ⊢ 𝑂 ∈ V
opthhausdorff.2 ⊢ 𝑇 ∈ V
opthhausdorff.3 ⊢ 𝑂 ≠ 𝑇
Assertion opthhausdorff ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

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