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

Theorem avril1 12976
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 3364 . . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13 0cn 7105 . . . . . . . 8 |- 0 e. CC
1413mulid1i 7107 . . . . . . 7 |- (0 x. 1) = 0
1514opeq2i 3201 . . . . . 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 7016 . . . . . . . 8 |- _i = <.0R, 1R>.
2120fveq1i 4678 . . . . . . 7 |- (_i` 1) = (<.0R, 1R>.` 1)
22 df-fv 4024 . . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2321, 22eqtri 1958 . . . . . 6 |- (_i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2423breq2i 3371 . . . . 5 |- (A~PRR(_i` 1) <-> A~PRRU.{y | (<.0R, 1R>."{1}) = {y}})
25 df-r 7017 . . . . . . 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 3068 . . . . . . . 8 |- ~PRR = {z | z C_ RR}
29 df-pw 3068 . . . . . . . 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 3369 . . . . 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 3066  {csn 3079  <.cop 3082  U.cuni 3218   class class class wbr 3363   X. cxp 3994  "cima 3999  ` cfv 4008  (class class class)co 4927  R.cnr 6757  0Rc0r 6758  1Rc1r 6759  RRcr 7006  0cc0 7007  1c1 7008  _ici 7009   x. cmul 7012
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 7061  ax-1cn 7062  ax-icn 7063  ax-addcl 7064  ax-mulcl 7066  ax-mulcom 7068  ax-mulass 7070  ax-distr 7071  ax-i2m1 7072  ax-1rid 7074  ax-cnre 7077
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 3068  df-sn 3085  df-pr 3086  df-op 3088  df-uni 3219  df-br 3364  df-opab 3418  df-xp 4010  df-cnv 4012  df-dm 4014  df-rn 4015  df-res 4016  df-ima 4017  df-fv 4024  df-ov 4929  df-i 7016  df-r 7017
Copyright terms: Public domain