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

Theorem opthwiener 4663
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 3951 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 22 . . . . . . 7  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
2 snex 4603 . . . . . . . . . . . 12  |-  { { B } }  e.  _V
32prid2 4053 . . . . . . . . . . 11  |-  { { B } }  e.  { { { A } ,  (/)
} ,  { { B } } }
4 eleq2 2455 . . . . . . . . . . 11  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( { { B } }  e.  { { { A } ,  (/)
} ,  { { B } } }  <->  { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } ) )
53, 4mpbii 211 . . . . . . . . . 10  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } )
62elpr 3962 . . . . . . . . . 10  |-  ( { { B } }  e.  { { { C } ,  (/) } ,  { { D } } } 
<->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
75, 6sylib 196 . . . . . . . . 9  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
8 0ex 4497 . . . . . . . . . . . . 13  |-  (/)  e.  _V
98prid2 4053 . . . . . . . . . . . 12  |-  (/)  e.  { { C } ,  (/) }
10 opthw.2 . . . . . . . . . . . . . 14  |-  B  e. 
_V
1110snnz 4062 . . . . . . . . . . . . 13  |-  { B }  =/=  (/)
128elsnc 3968 . . . . . . . . . . . . . 14  |-  ( (/)  e.  { { B } } 
<->  (/)  =  { B }
)
13 eqcom 2391 . . . . . . . . . . . . . 14  |-  ( (/)  =  { B }  <->  { B }  =  (/) )
1412, 13bitri 249 . . . . . . . . . . . . 13  |-  ( (/)  e.  { { B } } 
<->  { B }  =  (/) )
1511, 14nemtbir 2710 . . . . . . . . . . . 12  |-  -.  (/)  e.  { { B } }
16 nelneq2 2500 . . . . . . . . . . . 12  |-  ( (
(/)  e.  { { C } ,  (/) }  /\  -.  (/)  e.  { { B } } )  ->  -.  { { C } ,  (/) }  =  { { B } } )
179, 15, 16mp2an 670 . . . . . . . . . . 11  |-  -.  { { C } ,  (/) }  =  { { B } }
18 eqcom 2391 . . . . . . . . . . 11  |-  ( { { C } ,  (/)
}  =  { { B } }  <->  { { B } }  =  { { C } ,  (/) } )
1917, 18mtbi 296 . . . . . . . . . 10  |-  -.  { { B } }  =  { { C } ,  (/)
}
20 biorf 403 . . . . . . . . . 10  |-  ( -. 
{ { B } }  =  { { C } ,  (/) }  ->  ( { { B } }  =  { { D } }  <->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) ) )
2119, 20ax-mp 5 . . . . . . . . 9  |-  ( { { B } }  =  { { D } } 
<->  ( { { B } }  =  { { C } ,  (/) }  \/  { { B } }  =  { { D } } ) )
227, 21sylibr 212 . . . . . . . 8  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { B } }  =  { { D } } )
2322preq2d 4030 . . . . . . 7  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { C } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
241, 23eqtr4d 2426 . . . . . 6  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { B } } } )
25 prex 4604 . . . . . . 7  |-  { { A } ,  (/) }  e.  _V
26 prex 4604 . . . . . . 7  |-  { { C } ,  (/) }  e.  _V
2725, 26preqr1 4118 . . . . . 6  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { B } } }  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
2824, 27syl 16 . . . . 5  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
29 snex 4603 . . . . . 6  |-  { A }  e.  _V
30 snex 4603 . . . . . 6  |-  { C }  e.  _V
3129, 30preqr1 4118 . . . . 5  |-  ( { { A } ,  (/)
}  =  { { C } ,  (/) }  ->  { A }  =  { C } )
3228, 31syl 16 . . . 4  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { A }  =  { C } )
33 opthw.1 . . . . 5  |-  A  e. 
_V
3433sneqr 4111 . . . 4  |-  ( { A }  =  { C }  ->  A  =  C )
3532, 34syl 16 . . 3  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  A  =  C )
36 snex 4603 . . . . . 6  |-  { B }  e.  _V
3736sneqr 4111 . . . . 5  |-  ( { { B } }  =  { { D } }  ->  { B }  =  { D } )
3822, 37syl 16 . . . 4  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  { B }  =  { D } )
3910sneqr 4111 . . . 4  |-  ( { B }  =  { D }  ->  B  =  D )
4038, 39syl 16 . . 3  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  B  =  D )
4135, 40jca 530 . 2  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } }  ->  ( A  =  C  /\  B  =  D ) )
42 sneq 3954 . . . . 5  |-  ( A  =  C  ->  { A }  =  { C } )
4342preq1d 4029 . . . 4  |-  ( A  =  C  ->  { { A } ,  (/) }  =  { { C } ,  (/)
} )
4443preq1d 4029 . . 3  |-  ( A  =  C  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/)
} ,  { { B } } } )
45 sneq 3954 . . . . 5  |-  ( B  =  D  ->  { B }  =  { D } )
46 sneq 3954 . . . . 5  |-  ( { B }  =  { D }  ->  { { B } }  =  { { D } } )
4745, 46syl 16 . . . 4  |-  ( B  =  D  ->  { { B } }  =  { { D } } )
4847preq2d 4030 . . 3  |-  ( B  =  D  ->  { { { C } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/)
} ,  { { D } } } )
4944, 48sylan9eq 2443 . 2  |-  ( ( A  =  C  /\  B  =  D )  ->  { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } )
5041, 49impbii 188 1  |-  ( { { { A } ,  (/) } ,  { { B } } }  =  { { { C } ,  (/) } ,  { { D } } } 
<->  ( A  =  C  /\  B  =  D ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    \/ wo 366    /\ wa 367    = wceq 1399    e. wcel 1826   _Vcvv 3034   (/)c0 3711   {csn 3944   {cpr 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-v 3036  df-dif 3392  df-un 3394  df-nul 3712  df-sn 3945  df-pr 3947
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator