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

Theorem avril1 19368
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 1680 . . . . . . . 8  |-  x  =  x
2 dfnul2 3074 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2166 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 320 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 197 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2124 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 291 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2537 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 2483 . . . . . 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 3587 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 8251 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 8257 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3402 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2127 . . . . 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 842 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } }  /\  F (/) ( 0  x.  1 ) )
20 df-i 8167 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5045 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 4284 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
2321, 22eqtri 2084 . . . . . 6  |-  ( _i
`  1 )  = 
U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } }
2423breq2i 3594 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } } )
25 df-r 8168 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 2836 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2173 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3243 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3243 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2121 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 8 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 3592 . . . . 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 669 . . 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 1520    e. wcel 1522   {cab 2051   _Vcvv 2475    C_ wss 2793   (/)c0 3072   ~Pcpw 3241   {csn 3255   <.cop 3258   U.cuni 3424   class class class wbr 3586    X. cxp 4254   "cima 4259   ` cfv 4268  (class class class)co 5360   R.cnr 7910   0Rc0r 7911   1Rc1r 7912   RRcr 8157   0cc0 8158   1c1 8159   _ici 8160    x. cmul 8163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-7 1444  ax-gen 1445  ax-8 1524  ax-11 1525  ax-17 1529  ax-12o 1562  ax-10 1576  ax-9 1582  ax-4 1589  ax-16 1775  ax-ext 2046  ax-resscn 8214  ax-1cn 8215  ax-icn 8216  ax-addcl 8217  ax-mulcl 8219  ax-mulcom 8221  ax-mulass 8223  ax-distr 8224  ax-i2m1 8225  ax-1rid 8227  ax-cnre 8230
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 898  df-ex 1447  df-sb 1736  df-clab 2052  df-cleq 2057  df-clel 2060  df-ral 2278  df-rex 2279  df-rab 2281  df-v 2477  df-dif 2796  df-un 2798  df-in 2800  df-ss 2804  df-nul 3073  df-if 3182  df-pw 3243  df-sn 3261  df-pr 3262  df-op 3264  df-uni 3425  df-br 3587  df-opab 3641  df-xp 4270  df-cnv 4272  df-dm 4274  df-rn 4275  df-res 4276  df-ima 4277  df-fv 4284  df-ov 5363  df-i 8167  df-r 8168
Copyright terms: Public domain