HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem avril1 18151
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.)

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 1677 . . . . . . . 8  |-  x  =  x
2 dfnul2 3071 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2163 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 320 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 197 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2121 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 291 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2534 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 2480 . . . . . 6  |-  ( <. F ,  0 >.  e.  (/)  ->  <. F ,  0
>.  e.  _V )
109con3i 125 . . . . 5  |-  ( -. 
<. F ,  0 >.  e.  _V  ->  -.  <. F , 
0 >.  e.  (/) )
118, 10pm2.61i 154 . . . 4  |-  -.  <. F ,  0 >.  e.  (/)
12 df-br 3583 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 8250 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 8252 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3398 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2124 . . . . 5  |-  ( <. F ,  ( 0  x.  1 ) >.  e.  (/)  <->  <. F ,  0
>.  e.  (/) )
1712, 16bitri 238 . . . 4  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
0 >.  e.  (/) )
1811, 17mtbir 288 . . 3  |-  -.  F (/) ( 0  x.  1 )
1918intnan 839 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } }  /\  F (/) ( 0  x.  1 ) )
20 df-i 8156 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5039 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 4280 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
2321, 22eqtri 2081 . . . . . 6  |-  ( _i
`  1 )  = 
U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } }
2423breq2i 3590 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } } )
25 df-r 8157 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 2833 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2170 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3239 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3239 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2118 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 8 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 3588 . . . . 5  |-  ( A ~P RR U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }  <->  A ~P ( R.  X.  { 0R } ) U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } } )
3324, 32bitri 238 . . . 4  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P ( R.  X.  { 0R } ) U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
)
3433anbi1i 667 . . 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 285 . 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 198 1  |-  -.  ( A ~P RR ( _i
`  1 )  /\  F (/) ( 0  x.  1 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 356    = wceq 1517    e. wcel 1519   {cab 2048   _Vcvv 2472    C_ wss 2790   (/)c0 3069   ~Pcpw 3237   {csn 3251   <.cop 3254   U.cuni 3420   class class class wbr 3582    X. cxp 4250   "cima 4255   ` cfv 4264  (class class class)co 5353   R.cnr 7899   0Rc0r 7900   1Rc1r 7901   RRcr 8146   0cc0 8147   1c1 8148   _ici 8149    x. cmul 8152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586  ax-16 1772  ax-ext 2043  ax-resscn 8203  ax-1cn 8204  ax-icn 8205  ax-addcl 8206  ax-mulcl 8208  ax-mulcom 8210  ax-mulass 8212  ax-distr 8213  ax-i2m1 8214  ax-1rid 8216  ax-cnre 8219
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 895  df-ex 1444  df-sb 1733  df-clab 2049  df-cleq 2054  df-clel 2057  df-ral 2275  df-rex 2276  df-rab 2278  df-v 2474  df-dif 2793  df-un 2795  df-in 2797  df-ss 2801  df-nul 3070  df-if 3178  df-pw 3239  df-sn 3257  df-pr 3258  df-op 3260  df-uni 3421  df-br 3583  df-opab 3637  df-xp 4266  df-cnv 4268  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-fv 4280  df-ov 5356  df-i 8156  df-r 8157
Copyright terms: Public domain