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

Theorem avril1 20595
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 1818 . . . . . . . 8  |-  x  =  x
2 dfnul2 3361 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2356 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 324 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 201 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2313 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 295 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2790 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 2733 . . . . . 6  |-  ( <. F ,  0 >.  e.  (/)  ->  <. F ,  0
>.  e.  _V )
109con3i 129 . . . . 5  |-  ( -. 
<. F ,  0 >.  e.  _V  ->  -.  <. F , 
0 >.  e.  (/) )
118, 10pm2.61i 158 . . . 4  |-  -.  <. F ,  0 >.  e.  (/)
12 df-br 3918 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 8708 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 8716 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3697 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2316 . . . . 5  |-  ( <. F ,  ( 0  x.  1 ) >.  e.  (/)  <->  <. F ,  0
>.  e.  (/) )
1712, 16bitri 242 . . . 4  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
0 >.  e.  (/) )
1811, 17mtbir 292 . . 3  |-  -.  F (/) ( 0  x.  1 )
1918intnan 885 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } }  /\  F (/) ( 0  x.  1 ) )
20 df-i 8623 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5375 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 4605 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
2321, 22eqtri 2273 . . . . . 6  |-  ( _i
`  1 )  = 
U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } }
2423breq2i 3925 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } } )
25 df-r 8624 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 3118 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2363 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3529 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3529 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2310 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 10 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 3923 . . . . 5  |-  ( A ~P RR U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }  <->  A ~P ( R.  X.  { 0R } ) U. { y  |  (
<. 0R ,  1R >. " { 1 } )  =  { y } } )
3324, 32bitri 242 . . . 4  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P ( R.  X.  { 0R } ) U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
)
3433anbi1i 679 . . 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 289 . 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 202 1  |-  -.  ( A ~P RR ( _i
`  1 )  /\  F (/) ( 0  x.  1 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    /\ wa 360    = wceq 1619    e. wcel 1621   {cab 2239   _Vcvv 2725    C_ wss 3075   (/)c0 3359   ~Pcpw 3527   {csn 3541   <.cop 3544   U.cuni 3724   class class class wbr 3917    X. cxp 4575   "cima 4580   ` cfv 4589  (class class class)co 5707   R.cnr 8366   0Rc0r 8367   1Rc1r 8368   RRcr 8613   0cc0 8614   1c1 8615   _ici 8616    x. cmul 8619
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-resscn 8671  ax-1cn 8672  ax-icn 8673  ax-addcl 8674  ax-mulcl 8676  ax-mulcom 8678  ax-mulass 8680  ax-distr 8681  ax-i2m1 8682  ax-1rid 8684  ax-cnre 8687
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ral 2511  df-rex 2512  df-rab 2514  df-v 2727  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-if 3468  df-pw 3529  df-sn 3547  df-pr 3548  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-xp 4591  df-cnv 4593  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fv 4605  df-ov 5710  df-i 8623  df-r 8624
  Copyright terms: Public domain W3C validator