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

Theorem avril1 11695
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 1702 . . . . . . . 8 |- x = x
2 dfnul2 3050 . . . . . . . . . 10 |- (/) = {x | -. x = x}
32abeq2i 2184 . . . . . . . . 9 |- (x e. (/) <-> -. x = x)
43con2bii 371 . . . . . . . 8 |- (x = x <-> -. x e. (/))
51, 4mpbi 231 . . . . . . 7 |- -. x e. (/)
6 eleq1 2138 . . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
75, 6mtbii 343 . . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
87vtocleg 2550 . . . . 5 |- (<.F, 0>. e. _V -> -. <.F, 0>. e. (/))
9 elisset 2491 . . . . . 6 |- (<.F, 0>. e. (/) -> <.F, 0>. e. _V)
109con3i 139 . . . . 5 |- (-. <.F, 0>. e. _V -> -. <.F, 0>. e. (/))
118, 10pm2.61i 171 . . . 4 |- -. <.F, 0>. e. (/)
12 df-br 3493 . . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13 0cn 7187 . . . . . . . 8 |- 0 e. CC
1413mulid1i 7189 . . . . . . 7 |- (0 x. 1) = 0
1514opeq2i 3330 . . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
1615eleq1i 2141 . . . . 5 |- (<.F, (0 x. 1)>. e. (/) <-> <.F, 0>. e. (/))
1712, 16bitri 280 . . . 4 |- (F(/)(0 x. 1) <-> <.F, 0>. e. (/))
1811, 17mtbir 340 . . 3 |- -. F(/)(0 x. 1)
1918intnan 961 . 2 |- -. (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1))
20 df-i 7098 . . . . . . . 8 |- _i = <.0R, 1R>.
2120fveq1i 4800 . . . . . . 7 |- (_i` 1) = (<.0R, 1R>.` 1)
22 df-fv 4148 . . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2321, 22eqtri 2095 . . . . . 6 |- (_i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2423breq2i 3500 . . . . 5 |- (A~PRR(_i` 1) <-> A~PRRU.{y | (<.0R, 1R>."{1}) = {y}})
25 df-r 7099 . . . . . . 7 |- RR = (R. X. {0R})
26 sseq2 2825 . . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z C_ RR <-> z C_ (R. X. {0R})))
2726abbidv 2192 . . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z C_ RR} = {z | z C_ (R. X. {0R})})
28 df-pw 3205 . . . . . . . 8 |- ~PRR = {z | z C_ RR}
29 df-pw 3205 . . . . . . . 8 |- ~P(R. X. {0R}) = {z | z C_ (R. X. {0R})}
3027, 28, 293eqtr4g 2135 . . . . . . 7 |- (RR = (R. X. {0R}) -> ~PRR = ~P(R. X. {0R}))
3125, 30ax-mp 7 . . . . . 6 |- ~PRR = ~P(R. X. {0R})
3231breqi 3498 . . . . 5 |- (A~PRRU.{y | (<.0R, 1R>."{1}) = {y}} <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3324, 32bitri 280 . . . 4 |- (A~PRR(_i` 1) <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3433anbi1i 770 . . 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 336 . 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 232 1 |- -. (A~PRR(_i` 1) /\ F(/)(0 x. 1))
Colors of variables: wff set class
Syntax hints:  -. wn 2   /\ wa 412   = wceq 1573   e. wcel 1575  {cab 2062  _Vcvv 2482   C_ wss 2784  (/)c0 3048  ~Pcpw 3203  {csn 3216  <.cop 3218  U.cuni 3347   class class class wbr 3492   X. cxp 4118  "cima 4123  ` cfv 4132  (class class class)co 5050  R.cnr 6839  0Rc0r 6840  1Rc1r 6841  RRcr 7088  0cc0 7089  1c1 7090  _ici 7091   x. cmul 7094
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1497  ax-6 1498  ax-7 1499  ax-gen 1500  ax-8 1577  ax-10 1578  ax-11 1579  ax-12 1580  ax-14 1582  ax-17 1589  ax-9 1603  ax-4 1609  ax-16 1786  ax-ext 2057  ax-sep 3592  ax-nul 3602  ax-pr 3662  ax-resscn 7143  ax-1cn 7144  ax-icn 7145  ax-addcl 7146  ax-mulcl 7148  ax-mulcom 7150  ax-mulass 7152  ax-distr 7153  ax-i2m1 7154  ax-1rid 7156  ax-cnre 7159
This theorem depends on definitions:  df-bi 204  df-or 413  df-an 414  df-3an 1020  df-ex 1502  df-sb 1748  df-eu 1975  df-mo 1976  df-clab 2063  df-cleq 2068  df-clel 2071  df-ne 2203  df-ral 2297  df-rex 2298  df-v 2484  df-dif 2787  df-un 2789  df-in 2791  df-ss 2793  df-nul 3049  df-pw 3205  df-sn 3220  df-pr 3221  df-op 3224  df-uni 3348  df-br 3493  df-opab 3551  df-xp 4134  df-cnv 4136  df-dm 4138  df-rn 4139  df-res 4140  df-ima 4141  df-fv 4148  df-opr 5052  df-i 7098  df-r 7099
Copyright terms: Public domain