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 e. _V
opthhausdorff.b 
|- B e. _V
opthhausdorff.o 
|- A =/= O
opthhausdorff.n 
|- B =/= O
opthhausdorff.t 
|- B =/= T
opthhausdorff.1 
|- O e. _V
opthhausdorff.2 
|- T e. _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 e. _V
2 opthhausdorff.b 
 |-  B e. _V
3 opthhausdorff.o 
 |-  A =/= O
4 opthhausdorff.n 
 |-  B =/= O
5 opthhausdorff.t 
 |-  B =/= T
6 opthhausdorff.1 
 |-  O e. _V
7 opthhausdorff.2 
 |-  T e. _V
8 opthhausdorff.3 
 |-  O =/= T
9 prex 
 |-  { A , O } e. _V
10 prex 
 |-  { B , T } e. _V
11 1 6 pm3.2i 
 |-  ( A e. _V /\ O e. _V )
12 2 7 pm3.2i 
 |-  ( B e. _V /\ T e. _V )
13 11 12 pm3.2i 
 |-  ( ( A e. _V /\ O e. _V ) /\ ( B e. _V /\ T e. _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 e. _V /\ O e. _V ) /\ ( B e. _V /\ T e. _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 } e. _V /\ { B , T } e. _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 e. _V /\ O e. _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 e. _V /\ T e. _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 e. _V /\ O e. _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 e. _V /\ T e. _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 ) )