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

Theorem avril1 20838
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 1646 . . . . . . . 8  |-  x  =  x
2 dfnul2 3459 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2392 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 322 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 199 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2345 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 293 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2856 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 2798 . . . . . 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 4026 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 8833 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 8841 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3802 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2348 . . . . 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 8748 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5528 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 5265 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  ( iota y 1 <. 0R ,  1R >. y )
2321, 22eqtri 2305 . . . . . 6  |-  ( _i
`  1 )  =  ( iota y 1
<. 0R ,  1R >. y )
2423breq2i 4033 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR ( iota y 1
<. 0R ,  1R >. y ) )
25 df-r 8749 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 3202 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2399 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3629 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3629 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2342 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 8 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 4031 . . . . 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 1625    e. wcel 1686   {cab 2271   _Vcvv 2790    C_ wss 3154   (/)c0 3457   ~Pcpw 3627   {csn 3642   <.cop 3645   class class class wbr 4025    X. cxp 4689   iotacio 5219   ` cfv 5257  (class class class)co 5860   R.cnr 8491   0Rc0r 8492   1Rc1r 8493   RRcr 8738   0cc0 8739   1c1 8740   _ici 8741    x. cmul 8744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-mulcl 8801  ax-mulcom 8803  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1rid 8809  ax-cnre 8812
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863  df-i 8748  df-r 8749
  Copyright terms: Public domain W3C validator