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

Theorem opthwiener 4284
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 3662 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 19 . . . . . . 7  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
2 snex 4232 . . . . . . . . . . . 12  |-  { { B } }  e.  _V
32prid2 3748 . . . . . . . . . . 11  |-  { { B } }  e.  { { { A } ,  (/)
} ,  { { B } } }
4 eleq2 2357 . . . . . . . . . . 11  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( { { B } }  e.  { { { A } ,  (/)
} ,  { { B } } }  <->  { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } ) )
53, 4mpbii 202 . . . . . . . . . 10  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } )
62elpr 3671 . . . . . . . . . 10  |-  ( { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } 
<->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
75, 6sylib 188 . . . . . . . . 9  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
8 0ex 4166 . . . . . . . . . . . . 13  |-  (/)  e.  _V
98prid2 3748 . . . . . . . . . . . 12  |-  (/)  e.  { { C } ,  (/) }
10 opthw.2 . . . . . . . . . . . . . 14  |-  B  e. 
_V
1110snnz 3757 . . . . . . . . . . . . 13  |-  { B }  =/=  (/)
128elsnc 3676 . . . . . . . . . . . . . 14  |-  ( (/)  e.  { { B } } 
<->  (/)  =  { B }
)
13 eqcom 2298 . . . . . . . . . . . . . 14  |-  ( (/)  =  { B }  <->  { B }  =  (/) )
1412, 13bitri 240 . . . . . . . . . . . . 13  |-  ( (/)  e.  { { B } } 
<->  { B }  =  (/) )
1511, 14nemtbir 2547 . . . . . . . . . . . 12  |-  -.  (/)  e.  { { B } }
16 nelneq2 2395 . . . . . . . . . . . 12  |-  ( (
(/)  e.  { { C } ,  (/) }  /\  -.  (/)  e.  { { B } } )  ->  -.  { { C } ,  (/) }  =  { { B } } )
179, 15, 16mp2an 653 . . . . . . . . . . 11  |-  -.  { { C } ,  (/) }  =  { { B } }
18 eqcom 2298 . . . . . . . . . . 11  |-  ( { { C } ,  (/)
}  =  { { B } }  <->  { { B } }  =  { { C } ,  (/) } )
1917, 18mtbi 289 . . . . . . . . . 10  |-  -.  { { B } }  =  { { C } ,  (/)
}
20 biorf 394 . . . . . . . . . 10  |-  ( -. 
{ { B } }  =  { { C } ,  (/) }  ->  ( { { B } }  =  { { D } }  <->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) ) )
2119, 20ax-mp 8 . . . . . . . . 9  |-  ( { { B } }  =  { { D } } 
<->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
227, 21sylibr 203 . . . . . . . 8  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { B } }  =  { { D } } )
2322preq2d 3726 . . . . . . 7  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { C } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
241, 23eqtr4d 2331 . . . . . 6  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { B } } } )
25 prex 4233 . . . . . . 7  |-  { { A } ,  (/) }  e.  _V
26 prex 4233 . . . . . . 7  |-  { { C } ,  (/) }  e.  _V
2725, 26preqr1 3802 . . . . . 6  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { B } } }  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
2824, 27syl 15 . . . . 5  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
29 snex 4232 . . . . . 6  |-  { A }  e.  _V
30 snex 4232 . . . . . 6  |-  { C }  e.  _V
3129, 30preqr1 3802 . . . . 5  |-  ( { { A } ,  (/)
}  =  { { C } ,  (/) }  ->  { A }  =  { C } )
3228, 31syl 15 . . . 4  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { A }  =  { C } )
33 opthw.1 . . . . 5  |-  A  e. 
_V
3433sneqr 3796 . . . 4  |-  ( { A }  =  { C }  ->  A  =  C )
3532, 34syl 15 . . 3  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  A  =  C )
36 snex 4232 . . . . . 6  |-  { B }  e.  _V
3736sneqr 3796 . . . . 5  |-  ( { { B } }  =  { { D } }  ->  { B }  =  { D } )
3822, 37syl 15 . . . 4  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { B }  =  { D } )
3910sneqr 3796 . . . 4  |-  ( { B }  =  { D }  ->  B  =  D )
4038, 39syl 15 . . 3  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  B  =  D )
4135, 40jca 518 . 2  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( A  =  C  /\  B  =  D ) )
42 sneq 3664 . . . . 5  |-  ( A  =  C  ->  { A }  =  { C } )
4342preq1d 3725 . . . 4  |-  ( A  =  C  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
4443preq1d 3725 . . 3  |-  ( A  =  C  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/)
} ,  { { B } } } )
45 sneq 3664 . . . . 5  |-  ( B  =  D  ->  { B }  =  { D } )
46 sneq 3664 . . . . 5  |-  ( { B }  =  { D }  ->  { { B } }  =  { { D } } )
4745, 46syl 15 . . . 4  |-  ( B  =  D  ->  { { B } }  =  { { D } } )
4847preq2d 3726 . . 3  |-  ( B  =  D  ->  { { { C } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/)
} ,  { { D } } } )
4944, 48sylan9eq 2348 . 2  |-  ( ( A  =  C  /\  B  =  D )  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
5041, 49impbii 180 1  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } 
<->  ( A  =  C  /\  B  =  D ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1632    e. wcel 1696   _Vcvv 2801   (/)c0 3468   {csn 3653   {cpr 3654
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator