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

Theorem opthwiener 4205
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 3590 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 4154 . . . . . . . . . . . 12  |-  { { B } }  e.  _V
32prid2 3676 . . . . . . . . . . 11  |-  { { B } }  e.  { { { A } ,  (/)
} ,  { { B } } }
4 eleq2 2317 . . . . . . . . . . 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 3599 . . . . . . . . . 10  |-  ( { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } 
<->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
75, 6sylib 190 . . . . . . . . 9  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
8 0ex 4090 . . . . . . . . . . . . 13  |-  (/)  e.  _V
98prid2 3676 . . . . . . . . . . . 12  |-  (/)  e.  { { C } ,  (/) }
10 opthw.2 . . . . . . . . . . . . . 14  |-  B  e. 
_V
1110snnz 3685 . . . . . . . . . . . . 13  |-  { B }  =/=  (/)
128elsnc 3604 . . . . . . . . . . . . . 14  |-  ( (/)  e.  { { B } } 
<->  (/)  =  { B }
)
13 eqcom 2258 . . . . . . . . . . . . . 14  |-  ( (/)  =  { B }  <->  { B }  =  (/) )
1412, 13bitri 242 . . . . . . . . . . . . 13  |-  ( (/)  e.  { { B } } 
<->  { B }  =  (/) )
1511, 14nemtbir 2507 . . . . . . . . . . . 12  |-  -.  (/)  e.  { { B } }
16 nelneq2 2355 . . . . . . . . . . . 12  |-  ( (
(/)  e.  { { C } ,  (/) }  /\  -.  (/)  e.  { { B } } )  ->  -.  { { C } ,  (/) }  =  { { B } } )
179, 15, 16mp2an 656 . . . . . . . . . . 11  |-  -.  { { C } ,  (/) }  =  { { B } }
18 eqcom 2258 . . . . . . . . . . 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 3654 . . . . . . 7  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { C } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
241, 23eqtr4d 2291 . . . . . 6  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { B } } } )
25 prex 4155 . . . . . . 7  |-  { { A } ,  (/) }  e.  _V
26 prex 4155 . . . . . . 7  |-  { { C } ,  (/) }  e.  _V
2725, 26preqr1 3727 . . . . . 6  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { B } } }  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
2824, 27syl 17 . . . . 5  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
29 snex 4154 . . . . . 6  |-  { A }  e.  _V
30 snex 4154 . . . . . 6  |-  { C }  e.  _V
3129, 30preqr1 3727 . . . . 5  |-  ( { { A } ,  (/)
}  =  { { C } ,  (/) }  ->  { A }  =  { C } )
3228, 31syl 17 . . . 4  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { A }  =  { C } )
33 opthw.1 . . . . 5  |-  A  e. 
_V
3433sneqr 3721 . . . 4  |-  ( { A }  =  { C }  ->  A  =  C )
3532, 34syl 17 . . 3  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  A  =  C )
36 snex 4154 . . . . . 6  |-  { B }  e.  _V
3736sneqr 3721 . . . . 5  |-  ( { { B } }  =  { { D } }  ->  { B }  =  { D } )
3822, 37syl 17 . . . 4  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { B }  =  { D } )
3910sneqr 3721 . . . 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 3592 . . . . 5  |-  ( A  =  C  ->  { A }  =  { C } )
4342preq1d 3653 . . . 4  |-  ( A  =  C  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
4443preq1d 3653 . . 3  |-  ( A  =  C  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/)
} ,  { { B } } } )
45 sneq 3592 . . . . 5  |-  ( B  =  D  ->  { B }  =  { D } )
46 sneq 3592 . . . . 5  |-  ( { B }  =  { D }  ->  { { B } }  =  { { D } } )
4745, 46syl 17 . . . 4  |-  ( B  =  D  ->  { { B } }  =  { { D } } )
4847preq2d 3654 . . 3  |-  ( B  =  D  ->  { { { C } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/)
} ,  { { D } } } )
4944, 48sylan9eq 2308 . 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 2740   (/)c0 3397   {csn 3581   {cpr 3582
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 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2742  df-dif 3097  df-un 3099  df-nul 3398  df-sn 3587  df-pr 3588
  Copyright terms: Public domain W3C validator