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 
|- A e. _V
opthhausdorff0.b 
|- B e. _V
opthhausdorff0.c 
|- C e. _V
opthhausdorff0.d 
|- D e. _V
opthhausdorff0.1 
|- O e. _V
opthhausdorff0.2 
|- T e. _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 e. _V
2 opthhausdorff0.b 
 |-  B e. _V
3 opthhausdorff0.c 
 |-  C e. _V
4 opthhausdorff0.d 
 |-  D e. _V
5 opthhausdorff0.1 
 |-  O e. _V
6 opthhausdorff0.2 
 |-  T e. _V
7 opthhausdorff0.3 
 |-  O =/= T
8 prex 
 |-  { A , O } e. _V
9 prex 
 |-  { B , T } e. _V
10 prex 
 |-  { C , O } e. _V
11 prex 
 |-  { D , T } e. _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 ) )