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

Theorem avril1 12954
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.)

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~PRR(_i` 1) /\ F(/)(0 x. 1))

Proof of Theorem avril1
StepHypRef Expression
1 equid 1565 . . . . . . . 8 |- x = x
2 dfnul2 2908 . . . . . . . . . 10 |- (/) = {x | -. x = x}
32abeq2i 2039 . . . . . . . . 9 |- (x e. (/) <-> -. x = x)
43con2bii 323 . . . . . . . 8 |- (x = x <-> -. x e. (/))
51, 4mpbi 197 . . . . . . 7 |- -. x e. (/)
6 eleq1 1997 . . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
75, 6mtbii 293 . . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
87vtocleg 2405 . . . . 5 |- (<.F, 0>. e. _V -> -. <.F, 0>. e. (/))
9 elex 2351 . . . . . 6 |- (<.F, 0>. e. (/) -> <.F, 0>. e. _V)
109con3i 124 . . . . 5 |- (-. <.F, 0>. e. _V -> -. <.F, 0>. e. (/))
118, 10pm2.61i 153 . . . 4 |- -. <.F, 0>. e. (/)
12 df-br 3363 . . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13 0cn 7090 . . . . . . . 8 |- 0 e. CC
1413mulid1i 7092 . . . . . . 7 |- (0 x. 1) = 0
1514opeq2i 3200 . . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
1615eleq1i 2000 . . . . 5 |- (<.F, (0 x. 1)>. e. (/) <-> <.F, 0>. e. (/))
1712, 16bitri 239 . . . 4 |- (F(/)(0 x. 1) <-> <.F, 0>. e. (/))
1811, 17mtbir 290 . . 3 |- -. F(/)(0 x. 1)
1918intnan 866 . 2 |- -. (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1))
20 df-i 7001 . . . . . . . 8 |- _i = <.0R, 1R>.
2120fveq1i 4673 . . . . . . 7 |- (_i` 1) = (<.0R, 1R>.` 1)
22 df-fv 4023 . . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2321, 22eqtri 1958 . . . . . 6 |- (_i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2423breq2i 3370 . . . . 5 |- (A~PRR(_i` 1) <-> A~PRRU.{y | (<.0R, 1R>."{1}) = {y}})
25 df-r 7002 . . . . . . 7 |- RR = (R. X. {0R})
26 sseq2 2685 . . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z C_ RR <-> z C_ (R. X. {0R})))
2726abbidv 2047 . . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z C_ RR} = {z | z C_ (R. X. {0R})})
28 df-pw 3067 . . . . . . . 8 |- ~PRR = {z | z C_ RR}
29 df-pw 3067 . . . . . . . 8 |- ~P(R. X. {0R}) = {z | z C_ (R. X. {0R})}
3027, 28, 293eqtr4g 1994 . . . . . . 7 |- (RR = (R. X. {0R}) -> ~PRR = ~P(R. X. {0R}))
3125, 30ax-mp 8 . . . . . 6 |- ~PRR = ~P(R. X. {0R})
3231breqi 3368 . . . . 5 |- (A~PRRU.{y | (<.0R, 1R>."{1}) = {y}} <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3324, 32bitri 239 . . . 4 |- (A~PRR(_i` 1) <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3433anbi1i 681 . . 3 |- ((A~PRR(_i` 1) /\ F(/)(0 x. 1)) <-> (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1)))
3534notbii 287 . 2 |- (-. (A~PRR(_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~PRR(_i` 1) /\ F(/)(0 x. 1))
Colors of variables: wff set class
Syntax hints:  -. wn 3   /\ wa 361   = wceq 1434   e. wcel 1436  {cab 1925  _Vcvv 2343   C_ wss 2642  (/)c0 2906  ~Pcpw 3065  {csn 3078  <.cop 3081  U.cuni 3217   class class class wbr 3362   X. cxp 3993  "cima 3998  ` cfv 4007  (class class class)co 4922  R.cnr 6742  0Rc0r 6743  1Rc1r 6744  RRcr 6991  0cc0 6992  1c1 6993  _ici 6994   x. cmul 6997
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-resscn 7046  ax-1cn 7047  ax-icn 7048  ax-addcl 7049  ax-mulcl 7051  ax-mulcom 7053  ax-mulass 7055  ax-distr 7056  ax-i2m1 7057  ax-1rid 7059  ax-cnre 7062
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3an 923  df-ex 1356  df-sb 1611  df-clab 1926  df-cleq 1931  df-clel 1934  df-ral 2151  df-rex 2152  df-v 2345  df-dif 2645  df-un 2647  df-in 2649  df-ss 2651  df-nul 2907  df-pw 3067  df-sn 3084  df-pr 3085  df-op 3087  df-uni 3218  df-br 3363  df-opab 3417  df-xp 4009  df-cnv 4011  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fv 4023  df-ov 4924  df-i 7001  df-r 7002
Copyright terms: Public domain