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

Theorem avril1 18060
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 1698 . . . . . . . 8  |-  x  =  x
2 dfnul2 3090 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2183 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 321 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 197 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2141 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 291 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2554 . . . . 5  |-  ( <. F ,  0 >.  e.  _V  ->  -.  <. F ,  0
>.  e.  (/) )
9 elex 2500 . . . . . 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 3601 . . . . 5  |-  ( F (/) ( 0  x.  1 )  <->  <. F ,  ( 0  x.  1 )
>.  e.  (/) )
13 0cn 8240 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 8242 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3416 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2144 . . . . 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 844 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } }  /\  F (/) ( 0  x.  1 ) )
20 df-i 8146 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5043 . . . . . . 7  |-  ( _i `  1 )  =  (
<. 0R ,  1R >. `  1 )
22 df-fv 4303 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
2321, 22eqtri 2102 . . . . . 6  |-  ( _i `  1 )  =  U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } }
2423breq2i 3608 . . . . 5  |-  ( A ~P RR ( _i ` 
1 )  <->  A ~P RR U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } } )
25 df-r 8147 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 2853 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2190 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3260 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3260 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2138 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 8 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 3606 . . . . 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 672 . . 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 357    = wceq 1536    e. wcel 1538   {cab 2069   _Vcvv 2492    C_ wss 2810   (/)c0 3088   ~Pcpw 3258   {csn 3272   <.cop 3275   U.cuni 3438   class class class wbr 3600    X. cxp 4273   "cima 4278   ` cfv 4287  (class class class)co 5354   R.cnr 7889   0Rc0r 7890   1Rc1r 7891   RRcr 8136   0cc0 8137   1c1 8138   _ici 8139    x. cmul 8142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-resscn 8193  ax-1cn 8194  ax-icn 8195  ax-addcl 8196  ax-mulcl 8198  ax-mulcom 8200  ax-mulass 8202  ax-distr 8203  ax-i2m1 8204  ax-1rid 8206  ax-cnre 8209
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 905  df-ex 1456  df-sb 1754  df-clab 2070  df-cleq 2075  df-clel 2078  df-ral 2295  df-rex 2296  df-rab 2298  df-v 2494  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3089  df-if 3199  df-pw 3260  df-sn 3278  df-pr 3279  df-op 3281  df-uni 3439  df-br 3601  df-opab 3655  df-xp 4289  df-cnv 4291  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fv 4303  df-ov 5357  df-i 8146  df-r 8147
Copyright terms: Public domain