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

Theorem avril1 21268
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 german 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/mpeuni/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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 equid 1681 . . . . . . . 8  |-  x  =  x
2 dfnul2 3545 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2473 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 322 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 199 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2426 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 293 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2939 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 2881 . . . . . 6  |-  ( <. F ,  0 >.  e.  (/)  ->  <. F ,  0
>.  e.  _V )
109con3i 127 . . . . 5  |-  ( -. 
<. F ,  0 >.  e.  _V  ->  -.  <. F , 
0 >.  e.  (/) )
118, 10pm2.61i 156 . . . 4  |-  -.  <. F ,  0 >.  e.  (/)
12 df-br 4126 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 8978 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 8986 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3902 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2429 . . . . 5  |-  ( <. F ,  ( 0  x.  1 ) >.  e.  (/)  <->  <. F ,  0
>.  e.  (/) )
1712, 16bitri 240 . . . 4  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
0 >.  e.  (/) )
1811, 17mtbir 290 . . 3  |-  -.  F (/) ( 0  x.  1 )
1918intnan 880 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y
)  /\  F (/) ( 0  x.  1 ) )
20 df-i 8893 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5633 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 5366 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  ( iota y 1 <. 0R ,  1R >. y )
2321, 22eqtri 2386 . . . . . 6  |-  ( _i
`  1 )  =  ( iota y 1
<. 0R ,  1R >. y )
2423breq2i 4133 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR ( iota y 1
<. 0R ,  1R >. y ) )
25 df-r 8894 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 3286 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2480 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3716 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3716 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2423 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 8 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 4131 . . . . 5  |-  ( A ~P RR ( iota y 1 <. 0R ,  1R >. y )  <->  A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y ) )
3324, 32bitri 240 . . . 4  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y ) )
3433anbi1i 676 . . 3  |-  ( ( A ~P RR ( _i `  1 )  /\  F (/) ( 0  x.  1 ) )  <-> 
( A ~P ( R.  X.  { 0R }
) ( iota y
1 <. 0R ,  1R >. y )  /\  F (/) ( 0  x.  1 ) ) )
3534notbii 287 . 2  |-  ( -.  ( A ~P RR ( _i `  1 )  /\  F (/) ( 0  x.  1 ) )  <->  -.  ( A ~P ( R.  X.  { 0R }
) ( iota y
1 <. 0R ,  1R >. y )  /\  F (/) ( 0  x.  1 ) ) )
3619, 35mpbir 200 1  |-  -.  ( A ~P RR ( _i
`  1 )  /\  F (/) ( 0  x.  1 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 358    = wceq 1647    e. wcel 1715   {cab 2352   _Vcvv 2873    C_ wss 3238   (/)c0 3543   ~Pcpw 3714   {csn 3729   <.cop 3732   class class class wbr 4125    X. cxp 4790   iotacio 5320   ` cfv 5358  (class class class)co 5981   R.cnr 8636   0Rc0r 8637   1Rc1r 8638   RRcr 8883   0cc0 8884   1c1 8885   _ici 8886    x. cmul 8889
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-resscn 8941  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-mulcl 8946  ax-mulcom 8948  ax-mulass 8950  ax-distr 8951  ax-i2m1 8952  ax-1rid 8954  ax-cnre 8957
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366  df-ov 5984  df-i 8893  df-r 8894
  Copyright terms: Public domain W3C validator