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

Theorem avril1 11954
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 1587 . . . . . . . 8 |- x = x
2 dfnul2 2928 . . . . . . . . . 10 |- (/) = {x | -. x = x}
32abeq2i 2061 . . . . . . . . 9 |- (x e. (/) <-> -. x = x)
43con2bii 342 . . . . . . . 8 |- (x = x <-> -. x e. (/))
51, 4mpbi 217 . . . . . . 7 |- -. x e. (/)
6 eleq1 2019 . . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
75, 6mtbii 315 . . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
87vtocleg 2427 . . . . 5 |- (<.F, 0>. e. _V -> -. <.F, 0>. e. (/))
9 elex 2373 . . . . . 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 3377 . . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13 0cn 7058 . . . . . . . 8 |- 0 e. CC
1413mulid1i 7060 . . . . . . 7 |- (0 x. 1) = 0
1514opeq2i 3214 . . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
1615eleq1i 2022 . . . . 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 6969 . . . . . . . 8 |- _i = <.0R, 1R>.
2120fveq1i 4676 . . . . . . 7 |- (_i` 1) = (<.0R, 1R>.` 1)
22 df-fv 4028 . . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2321, 22eqtri 1980 . . . . . 6 |- (_i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2423breq2i 3384 . . . . 5 |- (A~PRR(_i` 1) <-> A~PRRU.{y | (<.0R, 1R>."{1}) = {y}})
25 df-r 6970 . . . . . . 7 |- RR = (R. X. {0R})
26 sseq2 2705 . . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z C_ RR <-> z C_ (R. X. {0R})))
2726abbidv 2069 . . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z C_ RR} = {z | z C_ (R. X. {0R})})
28 df-pw 3084 . . . . . . . 8 |- ~PRR = {z | z C_ RR}
29 df-pw 3084 . . . . . . . 8 |- ~P(R. X. {0R}) = {z | z C_ (R. X. {0R})}
3027, 28, 293eqtr4g 2016 . . . . . . 7 |- (RR = (R. X. {0R}) -> ~PRR = ~P(R. X. {0R}))
3125, 30ax-mp 8 . . . . . 6 |- ~PRR = ~P(R. X. {0R})
3231breqi 3382 . . . . 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 1947  _Vcvv 2365   C_ wss 2662  (/)c0 2926  ~Pcpw 3082  {csn 3095  <.cop 3097  U.cuni 3231   class class class wbr 3376   X. cxp 3998  "cima 4003  ` cfv 4012  (class class class)co 4924  R.cnr 6710  0Rc0r 6711  1Rc1r 6712  RRcr 6959  0cc0 6960  1c1 6961  _ici 6962   x. cmul 6965
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 1671  ax-ext 1942  ax-resscn 7014  ax-1cn 7015  ax-icn 7016  ax-addcl 7017  ax-mulcl 7019  ax-mulcom 7021  ax-mulass 7023  ax-distr 7024  ax-i2m1 7025  ax-1rid 7027  ax-cnre 7030
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3an 948  df-ex 1381  df-sb 1633  df-clab 1948  df-cleq 1953  df-clel 1956  df-ral 2173  df-rex 2174  df-v 2367  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-nul 2927  df-pw 3084  df-sn 3099  df-pr 3100  df-op 3103  df-uni 3232  df-br 3377  df-opab 3431  df-xp 4014  df-cnv 4016  df-dm 4018  df-rn 4019  df-res 4020  df-ima 4021  df-fv 4028  df-ov 4926  df-i 6969  df-r 6970
Copyright terms: Public domain