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

Theorem avril1 12560
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 1588 . . . . . . . 8 |- x = x
2 dfnul2 2929 . . . . . . . . . 10 |- (/) = {x | -. x = x}
32abeq2i 2062 . . . . . . . . 9 |- (x e. (/) <-> -. x = x)
43con2bii 342 . . . . . . . 8 |- (x = x <-> -. x e. (/))
51, 4mpbi 217 . . . . . . 7 |- -. x e. (/)
6 eleq1 2020 . . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
75, 6mtbii 315 . . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
87vtocleg 2428 . . . . 5 |- (<.F, 0>. e. _V -> -. <.F, 0>. e. (/))
9 elex 2374 . . . . . 6 |- (<.F, 0>. e. (/) -> <.F, 0>. e. _V)
109con3i 127 . . . . 5 |- (-. <.F, 0>. e. _V -> -. <.F, 0>. e. (/))
118, 10pm2.61i 158 . . . 4 |- -. <.F, 0>. e. (/)
12 df-br 3380 . . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13 0cn 7097 . . . . . . . 8 |- 0 e. CC
1413mulid1i 7099 . . . . . . 7 |- (0 x. 1) = 0
1514opeq2i 3217 . . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
1615eleq1i 2023 . . . . 5 |- (<.F, (0 x. 1)>. e. (/) <-> <.F, 0>. e. (/))
1712, 16bitri 259 . . . 4 |- (F(/)(0 x. 1) <-> <.F, 0>. e. (/))
1811, 17mtbir 312 . . 3 |- -. F(/)(0 x. 1)
1918intnan 890 . 2 |- -. (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1))
20 df-i 7008 . . . . . . . 8 |- _i = <.0R, 1R>.
2120fveq1i 4686 . . . . . . 7 |- (_i` 1) = (<.0R, 1R>.` 1)
22 df-fv 4036 . . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2321, 22eqtri 1981 . . . . . 6 |- (_i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2423breq2i 3387 . . . . 5 |- (A~PRR(_i` 1) <-> A~PRRU.{y | (<.0R, 1R>."{1}) = {y}})
25 df-r 7009 . . . . . . 7 |- RR = (R. X. {0R})
26 sseq2 2706 . . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z C_ RR <-> z C_ (R. X. {0R})))
2726abbidv 2070 . . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z C_ RR} = {z | z C_ (R. X. {0R})})
28 df-pw 3087 . . . . . . . 8 |- ~PRR = {z | z C_ RR}
29 df-pw 3087 . . . . . . . 8 |- ~P(R. X. {0R}) = {z | z C_ (R. X. {0R})}
3027, 28, 293eqtr4g 2017 . . . . . . 7 |- (RR = (R. X. {0R}) -> ~PRR = ~P(R. X. {0R}))
3125, 30ax-mp 8 . . . . . 6 |- ~PRR = ~P(R. X. {0R})
3231breqi 3385 . . . . 5 |- (A~PRRU.{y | (<.0R, 1R>."{1}) = {y}} <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3324, 32bitri 259 . . . 4 |- (A~PRR(_i` 1) <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3433anbi1i 704 . . 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 309 . 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 218 1 |- -. (A~PRR(_i` 1) /\ F(/)(0 x. 1))
Colors of variables: wff set class
Syntax hints:  -. wn 3   /\ wa 382   = wceq 1457   e. wcel 1459  {cab 1948  _Vcvv 2366   C_ wss 2663  (/)c0 2927  ~Pcpw 3085  {csn 3098  <.cop 3100  U.cuni 3234   class class class wbr 3379   X. cxp 4006  "cima 4011  ` cfv 4020  (class class class)co 4935  R.cnr 6749  0Rc0r 6750  1Rc1r 6751  RRcr 6998  0cc0 6999  1c1 7000  _ici 7001   x. cmul 7004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1672  ax-ext 1943  ax-resscn 7053  ax-1cn 7054  ax-icn 7055  ax-addcl 7056  ax-mulcl 7058  ax-mulcom 7060  ax-mulass 7062  ax-distr 7063  ax-i2m1 7064  ax-1rid 7066  ax-cnre 7069
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3an 948  df-ex 1381  df-sb 1634  df-clab 1949  df-cleq 1954  df-clel 1957  df-ral 2174  df-rex 2175  df-v 2368  df-dif 2666  df-un 2668  df-in 2670  df-ss 2672  df-nul 2928  df-pw 3087  df-sn 3102  df-pr 3103  df-op 3106  df-uni 3235  df-br 3380  df-opab 3434  df-xp 4022  df-cnv 4024  df-dm 4026  df-rn 4027  df-res 4028  df-ima 4029  df-fv 4036  df-ov 4937  df-i 7008  df-r 7009
Copyright terms: Public domain