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

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

Proof

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