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

Theorem avril1 11659
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 1719 . . . . . . . 8 |- x = x
2 dfnul2 3067 . . . . . . . . . 10 |- (/) = {x | -. x = x}
32abeq2i 2201 . . . . . . . . 9 |- (x e. (/) <-> -. x = x)
43con2bii 377 . . . . . . . 8 |- (x = x <-> -. x e. (/))
51, 4mpbi 237 . . . . . . 7 |- -. x e. (/)
6 eleq1 2155 . . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
75, 6mtbii 349 . . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
87vtocleg 2567 . . . . 5 |- (<.F, 0>. e. _V -> -. <.F, 0>. e. (/))
9 elisset 2508 . . . . . 6 |- (<.F, 0>. e. (/) -> <.F, 0>. e. _V)
109con3i 142 . . . . 5 |- (-. <.F, 0>. e. _V -> -. <.F, 0>. e. (/))
118, 10pm2.61i 175 . . . 4 |- -. <.F, 0>. e. (/)
12 df-br 3510 . . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13 0cn 7204 . . . . . . . 8 |- 0 e. CC
1413mulid1i 7206 . . . . . . 7 |- (0 x. 1) = 0
1514opeq2i 3347 . . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
1615eleq1i 2158 . . . . 5 |- (<.F, (0 x. 1)>. e. (/) <-> <.F, 0>. e. (/))
1712, 16bitri 286 . . . 4 |- (F(/)(0 x. 1) <-> <.F, 0>. e. (/))
1811, 17mtbir 346 . . 3 |- -. F(/)(0 x. 1)
1918intnan 980 . 2 |- -. (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1))
20 df-i 7115 . . . . . . . 8 |- _i = <.0R, 1R>.
2120fveq1i 4817 . . . . . . 7 |- (_i` 1) = (<.0R, 1R>.` 1)
22 df-fv 4165 . . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2321, 22eqtri 2112 . . . . . 6 |- (_i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2423breq2i 3517 . . . . 5 |- (A~PRR(_i` 1) <-> A~PRRU.{y | (<.0R, 1R>."{1}) = {y}})
25 df-r 7116 . . . . . . 7 |- RR = (R. X. {0R})
26 sseq2 2842 . . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z C_ RR <-> z C_ (R. X. {0R})))
2726abbidv 2209 . . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z C_ RR} = {z | z C_ (R. X. {0R})})
28 df-pw 3222 . . . . . . . 8 |- ~PRR = {z | z C_ RR}
29 df-pw 3222 . . . . . . . 8 |- ~P(R. X. {0R}) = {z | z C_ (R. X. {0R})}
3027, 28, 293eqtr4g 2152 . . . . . . 7 |- (RR = (R. X. {0R}) -> ~PRR = ~P(R. X. {0R}))
3125, 30ax-mp 7 . . . . . 6 |- ~PRR = ~P(R. X. {0R})
3231breqi 3515 . . . . 5 |- (A~PRRU.{y | (<.0R, 1R>."{1}) = {y}} <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3324, 32bitri 286 . . . 4 |- (A~PRR(_i` 1) <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3433anbi1i 787 . . 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 342 . 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 238 1 |- -. (A~PRR(_i` 1) /\ F(/)(0 x. 1))
Colors of variables: wff set class
Syntax hints:  -. wn 2   /\ wa 418   = wceq 1592   e. wcel 1594  {cab 2079  _Vcvv 2499   C_ wss 2801  (/)c0 3065  ~Pcpw 3220  {csn 3233  <.cop 3235  U.cuni 3364   class class class wbr 3509   X. cxp 4135  "cima 4140  ` cfv 4149  (class class class)co 5067  R.cnr 6856  0Rc0r 6857  1Rc1r 6858  RRcr 7105  0cc0 7106  1c1 7107  _ici 7108   x. cmul 7111
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-sep 3609  ax-nul 3619  ax-pr 3679  ax-resscn 7160  ax-1cn 7161  ax-icn 7162  ax-addcl 7163  ax-mulcl 7165  ax-mulcom 7167  ax-mulass 7169  ax-distr 7170  ax-i2m1 7171  ax-1rid 7173  ax-cnre 7176
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-v 2501  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-nul 3066  df-pw 3222  df-sn 3237  df-pr 3238  df-op 3241  df-uni 3365  df-br 3510  df-opab 3568  df-xp 4151  df-cnv 4153  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fv 4165  df-opr 5069  df-i 7115  df-r 7116
Copyright terms: Public domain