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

Theorem avril1 19387
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 1681 . . . . . . . 8  |-  x  =  x
2 dfnul2 3075 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2167 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 320 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 197 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2125 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 291 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2538 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 2484 . . . . . 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 3593 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 8257 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 8265 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3407 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2128 . . . . 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 8173 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5051 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 4290 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  U. {
y  |  ( <. 0R ,  1R >. " {
1 } )  =  { y } }
2321, 22eqtri 2085 . . . . . 6  |-  ( _i
`  1 )  = 
U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } }
2423breq2i 3600 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR U. { y  |  ( <. 0R ,  1R >. " { 1 } )  =  { y } } )
25 df-r 8174 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 2837 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2174 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3244 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3244 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2122 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 8 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 3598 . . . . 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 2052   _Vcvv 2476    C_ wss 2794   (/)c0 3073   ~Pcpw 3242   {csn 3256   <.cop 3259   U.cuni 3430   class class class wbr 3592    X. cxp 4260   "cima 4265   ` cfv 4274  (class class class)co 5366   R.cnr 7916   0Rc0r 7917   1Rc1r 7918   RRcr 8163   0cc0 8164   1c1 8165   _ici 8166    x. cmul 8169
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 1563  ax-10 1577  ax-9 1583  ax-4 1590  ax-16 1776  ax-ext 2047  ax-resscn 8220  ax-1cn 8221  ax-icn 8222  ax-addcl 8223  ax-mulcl 8225  ax-mulcom 8227  ax-mulass 8229  ax-distr 8230  ax-i2m1 8231  ax-1rid 8233  ax-cnre 8236
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 898  df-ex 1447  df-sb 1737  df-clab 2053  df-cleq 2058  df-clel 2061  df-ral 2279  df-rex 2280  df-rab 2282  df-v 2478  df-dif 2797  df-un 2799  df-in 2801  df-ss 2805  df-nul 3074  df-if 3183  df-pw 3244  df-sn 3262  df-pr 3263  df-op 3265  df-uni 3431  df-br 3593  df-opab 3647  df-xp 4276  df-cnv 4278  df-dm 4280  df-rn 4281  df-res 4282  df-ima 4283  df-fv 4290  df-ov 5369  df-i 8173  df-r 8174
Copyright terms: Public domain