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

Theorem avril1 20472
Description: Poisson d'Avril's Theorem. This theorem is noted for its Selbstdokumentieren property, which means, literally, "self-documenting" and recalls the principle of quidquid germanus dictum sit, altum viditur, often used in set theory. Starting with the seemingly simple yet profound fact that any object  x equals itself (proved by Tarski in 1965; see Lemma 6 of [Tarski] p. 68), we demonstrate that the power set of the real numbers, as a relation on the value of the imaginary unit, does not conjoin with an empty relation on the product of the additive and multiplicative identity elements, leading to this startling conclusion that has left even seasoned professional mathematicians scratching their heads. (Contributed by Prof. Loof Lirpa, 1-Apr-2005.) (Proof modification is discouraged.) (New usage is discouraged.)

A reply to skeptics can be found at http://us.metamath.org/mpegif/mmnotes.txt, under the 1-Apr-2006 entry.

Assertion
Ref Expression
avril1  |-  -.  ( A ~P RR ( _i
`  1 )  /\  F (/) ( 0  x.  1 ) )

Proof of Theorem avril1
StepHypRef Expression
1 equid 1807 . . . . . . . 8  |-  x  =  x
2 dfnul2 3344 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2344 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 321 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 198 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2301 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 292 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2777 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 2720 . . . . . 6  |-  ( <. F ,  0 >.  e.  (/)  ->  <. F ,  0
>.  e.  _V )
109con3i 126 . . . . 5  |-  ( -. 
<. F ,  0 >.  e.  _V  ->  -.  <. F , 
0 >.  e.  (/) )
118, 10pm2.61i 155 . . . 4  |-  -.  <. F ,  0 >.  e.  (/)
12 df-br 3901 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 8685 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 8693 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3680 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2304 . . . . 5  |-  ( <. F ,  ( 0  x.  1 ) >.  e.  (/)  <->  <. F ,  0
>.  e.  (/) )
1712, 16bitri 239 . . . 4  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
0 >.  e.  (/) )
1811, 17mtbir 289 . . 3  |-  -.  F (/) ( 0  x.  1 )
1918intnan 879 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } }  /\  F (/) ( 0  x.  1 ) )
20 df-i 8600 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5353 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 4587 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
2321, 22eqtri 2261 . . . . . 6  |-  ( _i
`  1 )  = 
U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } }
2423breq2i 3908 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } } )
25 df-r 8601 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 3101 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2351 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3512 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3512 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2298 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 9 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 3906 . . . . 5  |-  ( A ~P RR U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }  <->  A ~P ( R.  X.  { 0R } ) U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } } )
3324, 32bitri 239 . . . 4  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P ( R.  X.  { 0R } ) U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
)
3433anbi1i 673 . . 3  |-  ( ( A ~P RR ( _i `  1 )  /\  F (/) ( 0  x.  1 ) )  <-> 
( A ~P ( R.  X.  { 0R }
) U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } }  /\  F (/) ( 0  x.  1 ) ) )
3534notbii 286 . 2  |-  ( -.  ( A ~P RR ( _i `  1 )  /\  F (/) ( 0  x.  1 ) )  <->  -.  ( A ~P ( R.  X.  { 0R }
) U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } }  /\  F (/) ( 0  x.  1 ) ) )
3619, 35mpbir 199 1  |-  -.  ( A ~P RR ( _i
`  1 )  /\  F (/) ( 0  x.  1 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 4    /\ wa 357    = wceq 1608    e. wcel 1610   {cab 2227   _Vcvv 2712    C_ wss 3058   (/)c0 3342   ~Pcpw 3510   {csn 3524   <.cop 3527   U.cuni 3707   class class class wbr 3900    X. cxp 4557   "cima 4562   ` cfv 4571  (class class class)co 5685   R.cnr 8343   0Rc0r 8344   1Rc1r 8345   RRcr 8590   0cc0 8591   1c1 8592   _ici 8593    x. cmul 8596
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9  ax-5 1522  ax-6 1523  ax-7 1524  ax-gen 1525  ax-8 1612  ax-11 1613  ax-17 1617  ax-12o 1653  ax-10 1667  ax-9 1673  ax-4 1681  ax-16 1915  ax-ext 2222  ax-resscn 8648  ax-1cn 8649  ax-icn 8650  ax-addcl 8651  ax-mulcl 8653  ax-mulcom 8655  ax-mulass 8657  ax-distr 8658  ax-i2m1 8659  ax-1rid 8661  ax-cnre 8664
This theorem depends on definitions:  df-bi 176  df-or 358  df-an 359  df-3an 935  df-tru 1309  df-ex 1527  df-nf 1529  df-sb 1872  df-clab 2228  df-cleq 2234  df-clel 2237  df-nfc 2362  df-ral 2499  df-rex 2500  df-rab 2502  df-v 2714  df-dif 3061  df-un 3063  df-in 3065  df-ss 3069  df-nul 3343  df-if 3451  df-pw 3512  df-sn 3530  df-pr 3531  df-op 3533  df-uni 3708  df-br 3901  df-opab 3955  df-xp 4573  df-cnv 4575  df-dm 4577  df-rn 4578  df-res 4579  df-ima 4580  df-fv 4587  df-ov 5688  df-i 8600  df-r 8601
  Copyright terms: Public domain W3C validator