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

Theorem avril1 23828
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 1731 . . . . . . . 8  |-  x  =  x
2 dfnul2 3750 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2581 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 332 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 208 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2526 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 302 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 3149 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 3087 . . . . . 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 4404 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 9492 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 9502 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 4174 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2531 . . . . 5  |-  ( <. F ,  ( 0  x.  1 ) >.  e.  (/)  <->  <. F ,  0
>.  e.  (/) )
1712, 16bitri 249 . . . 4  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
0 >.  e.  (/) )
1811, 17mtbir 299 . . 3  |-  -.  F (/) ( 0  x.  1 )
1918intnan 905 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y
)  /\  F (/) ( 0  x.  1 ) )
20 df-i 9405 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5803 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 5537 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  ( iota y 1 <. 0R ,  1R >. y )
2321, 22eqtri 2483 . . . . . 6  |-  ( _i
`  1 )  =  ( iota y 1
<. 0R ,  1R >. y )
2423breq2i 4411 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR ( iota y 1
<. 0R ,  1R >. y ) )
25 df-r 9406 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 3489 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2590 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3973 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3973 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2520 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 5 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 4409 . . . . 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 695 . . 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 296 . 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 369    = wceq 1370    e. wcel 1758   {cab 2439   _Vcvv 3078    C_ wss 3439   (/)c0 3748   ~Pcpw 3971   {csn 3988   <.cop 3994   class class class wbr 4403    X. cxp 4949   iotacio 5490   ` cfv 5529  (class class class)co 6203   R.cnr 9148   0Rc0r 9149   1Rc1r 9150   RRcr 9395   0cc0 9396   1c1 9397   _ici 9398    x. cmul 9401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-resscn 9453  ax-1cn 9454  ax-icn 9455  ax-addcl 9456  ax-mulcl 9458  ax-mulcom 9460  ax-mulass 9462  ax-distr 9463  ax-i2m1 9464  ax-1rid 9466  ax-cnre 9469
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-iota 5492  df-fv 5537  df-ov 6206  df-i 9405  df-r 9406
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator