MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opthwiener Unicode version

Theorem opthwiener 4161
Description: Justification theorem for the ordered pair definition in Norbert Wiener, "A simplification of the logic of relations," Proc. of the Cambridge Philos. Soc., 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e. are not proper classes). See df-op 3553 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.)
Hypotheses
Ref Expression
opthw.1  |-  A  e. 
_V
opthw.2  |-  B  e. 
_V
Assertion
Ref Expression
opthwiener  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } 
<->  ( A  =  C  /\  B  =  D ) )

Proof of Theorem opthwiener
StepHypRef Expression
1 id 21 . . . . . . 7  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
2 snex 4110 . . . . . . . . . . . 12  |-  { { B } }  e.  _V
32prid2 3639 . . . . . . . . . . 11  |-  { { B } }  e.  { { { A } ,  (/)
} ,  { { B } } }
4 eleq2 2314 . . . . . . . . . . 11  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( { { B } }  e.  { { { A } ,  (/)
} ,  { { B } } }  <->  { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } ) )
53, 4mpbii 204 . . . . . . . . . 10  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } )
62elpr 3562 . . . . . . . . . 10  |-  ( { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } 
<->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
75, 6sylib 190 . . . . . . . . 9  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
8 0ex 4047 . . . . . . . . . . . . 13  |-  (/)  e.  _V
98prid2 3639 . . . . . . . . . . . 12  |-  (/)  e.  { { C } ,  (/) }
10 opthw.2 . . . . . . . . . . . . . 14  |-  B  e. 
_V
1110snnz 3648 . . . . . . . . . . . . 13  |-  { B }  =/=  (/)
128elsnc 3567 . . . . . . . . . . . . . 14  |-  ( (/)  e.  { { B } } 
<->  (/)  =  { B }
)
13 eqcom 2255 . . . . . . . . . . . . . 14  |-  ( (/)  =  { B }  <->  { B }  =  (/) )
1412, 13bitri 242 . . . . . . . . . . . . 13  |-  ( (/)  e.  { { B } } 
<->  { B }  =  (/) )
1511, 14nemtbir 2500 . . . . . . . . . . . 12  |-  -.  (/)  e.  { { B } }
16 nelneq2 2348 . . . . . . . . . . . 12  |-  ( (
(/)  e.  { { C } ,  (/) }  /\  -.  (/)  e.  { { B } } )  ->  -.  { { C } ,  (/) }  =  { { B } } )
179, 15, 16mp2an 656 . . . . . . . . . . 11  |-  -.  { { C } ,  (/) }  =  { { B } }
18 eqcom 2255 . . . . . . . . . . 11  |-  ( { { C } ,  (/)
}  =  { { B } }  <->  { { B } }  =  { { C } ,  (/) } )
1917, 18mtbi 291 . . . . . . . . . 10  |-  -.  { { B } }  =  { { C } ,  (/)
}
20 biorf 396 . . . . . . . . . 10  |-  ( -. 
{ { B } }  =  { { C } ,  (/) }  ->  ( { { B } }  =  { { D } }  <->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) ) )
2119, 20ax-mp 10 . . . . . . . . 9  |-  ( { { B } }  =  { { D } } 
<->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
227, 21sylibr 205 . . . . . . . 8  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { B } }  =  { { D } } )
2322preq2d 3617 . . . . . . 7  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { C } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
241, 23eqtr4d 2288 . . . . . 6  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { B } } } )
25 prex 4111 . . . . . . 7  |-  { { A } ,  (/) }  e.  _V
26 prex 4111 . . . . . . 7  |-  { { C } ,  (/) }  e.  _V
2725, 26preqr1 3686 . . . . . 6  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { B } } }  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
2824, 27syl 17 . . . . 5  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
29 snex 4110 . . . . . 6  |-  { A }  e.  _V
30 snex 4110 . . . . . 6  |-  { C }  e.  _V
3129, 30preqr1 3686 . . . . 5  |-  ( { { A } ,  (/)
}  =  { { C } ,  (/) }  ->  { A }  =  { C } )
3228, 31syl 17 . . . 4  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { A }  =  { C } )
33 opthw.1 . . . . 5  |-  A  e. 
_V
3433sneqr 3680 . . . 4  |-  ( { A }  =  { C }  ->  A  =  C )
3532, 34syl 17 . . 3  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  A  =  C )
36 snex 4110 . . . . . 6  |-  { B }  e.  _V
3736sneqr 3680 . . . . 5  |-  ( { { B } }  =  { { D } }  ->  { B }  =  { D } )
3822, 37syl 17 . . . 4  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { B }  =  { D } )
3910sneqr 3680 . . . 4  |-  ( { B }  =  { D }  ->  B  =  D )
4038, 39syl 17 . . 3  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  B  =  D )
4135, 40jca 520 . 2  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( A  =  C  /\  B  =  D ) )
42 sneq 3555 . . . . 5  |-  ( A  =  C  ->  { A }  =  { C } )
4342preq1d 3616 . . . 4  |-  ( A  =  C  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
4443preq1d 3616 . . 3  |-  ( A  =  C  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/)
} ,  { { B } } } )
45 sneq 3555 . . . . 5  |-  ( B  =  D  ->  { B }  =  { D } )
46 sneq 3555 . . . . 5  |-  ( { B }  =  { D }  ->  { { B } }  =  { { D } } )
4745, 46syl 17 . . . 4  |-  ( B  =  D  ->  { { B } }  =  { { D } } )
4847preq2d 3617 . . 3  |-  ( B  =  D  ->  { { { C } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/)
} ,  { { D } } } )
4944, 48sylan9eq 2305 . 2  |-  ( ( A  =  C  /\  B  =  D )  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
5041, 49impbii 182 1  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } 
<->  ( A  =  C  /\  B  =  D ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178    \/ wo 359    /\ wa 360    = wceq 1619    e. wcel 1621   _Vcvv 2727   (/)c0 3362   {csn 3544   {cpr 3545
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-un 3083  df-nul 3363  df-sn 3550  df-pr 3551
  Copyright terms: Public domain W3C validator