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

Theorem avril1 25588
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 1815 . . . . . . . 8  |-  x  =  x
2 dfnul2 3740 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2529 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 330 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 208 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2474 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 300 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 3130 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 3068 . . . . . 6  |-  ( <. F ,  0 >.  e.  (/)  ->  <. F ,  0
>.  e.  _V )
109con3i 135 . . . . 5  |-  ( -. 
<. F ,  0 >.  e.  _V  ->  -.  <. F , 
0 >.  e.  (/) )
118, 10pm2.61i 164 . . . 4  |-  -.  <. F ,  0 >.  e.  (/)
12 df-br 4396 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 9618 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 9628 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 4163 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2479 . . . . 5  |-  ( <. F ,  ( 0  x.  1 ) >.  e.  (/)  <->  <. F ,  0
>.  e.  (/) )
1712, 16bitri 249 . . . 4  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
0 >.  e.  (/) )
1811, 17mtbir 297 . . 3  |-  -.  F (/) ( 0  x.  1 )
1918intnan 915 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y
)  /\  F (/) ( 0  x.  1 ) )
20 df-i 9531 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5850 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 5577 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  ( iota y 1 <. 0R ,  1R >. y )
2321, 22eqtri 2431 . . . . . 6  |-  ( _i
`  1 )  =  ( iota y 1
<. 0R ,  1R >. y )
2423breq2i 4403 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR ( iota y 1
<. 0R ,  1R >. y ) )
25 df-r 9532 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 3464 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2538 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3957 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3957 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2468 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 5 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 4401 . . . . 5  |-  ( A ~P RR ( iota y 1 <. 0R ,  1R >. y )  <->  A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y ) )
3324, 32bitri 249 . . . 4  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y ) )
3433anbi1i 693 . . 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 294 . 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 209 1  |-  -.  ( A ~P RR ( _i
`  1 )  /\  F (/) ( 0  x.  1 ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 367    = wceq 1405    e. wcel 1842   {cab 2387   _Vcvv 3059    C_ wss 3414   (/)c0 3738   ~Pcpw 3955   {csn 3972   <.cop 3978   class class class wbr 4395    X. cxp 4821   iotacio 5531   ` cfv 5569  (class class class)co 6278   R.cnr 9273   0Rc0r 9274   1Rc1r 9275   RRcr 9521   0cc0 9522   1c1 9523   _ici 9524    x. cmul 9527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-mulcl 9584  ax-mulcom 9586  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1rid 9592  ax-cnre 9595
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-iota 5533  df-fv 5577  df-ov 6281  df-i 9531  df-r 9532
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator