Theorem avril1 11171

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

Step	Hyp	Ref	Expression
1		equid 1795	. . . . . . . 8 |- x = x
2		dfnul2 3116	. . . . . . . . . 10 |- (/) = {x | -. x = x}
3	2	abeq2i 2279	. . . . . . . . 9 |- (x e. (/) <-> -. x = x)
4	3	con2bii 395	. . . . . . . 8 |- (x = x <-> -. x e. (/))
5	1, 4	mpbi 254	. . . . . . 7 |- -. x e. (/)
6		eleq1 2233	. . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
7	5, 6	mtbii 371	. . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
8	7	vtocleg 2627	. . . . 5 |- (<.F, 0>. e. _V -> -. <.F, 0>. e. (/))
9		elisset 2578	. . . . . 6 |- (<.F, 0>. e. (/) -> <.F, 0>. e. _V)
10	9	con3i 161	. . . . 5 |- (-. <.F, 0>. e. _V -> -. <.F, 0>. e. (/))
11	8, 10	pm2.61i 201	. . . 4 |- -. <.F, 0>. e. (/)
12		df-br 3540	. . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13		0cn 6933	. . . . . . . 8 |- 0 e. CC
14	13	mulid1i 6935	. . . . . . 7 |- (0 x. 1) = 0
15	14	opeq2i 3381	. . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
16	15	eleq1i 2236	. . . . 5 |- (<.F, (0 x. 1)>. e. (/) <-> <.F, 0>. e. (/))
17	12, 16	bitri 306	. . . 4 |- (F(/)(0 x. 1) <-> <.F, 0>. e. (/))
18	11, 17	mtbir 367	. . 3 |- -. F(/)(0 x. 1)
19	18	intnan 1056	. 2 |- -. (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1))
20		df-i 6838	. . . . . . . 8 |- _i = <.0R, 1R>.
21	20	fveq1i 4805	. . . . . . 7 |- (_i` 1) = (<.0R, 1R>.` 1)
22		df-fv 4179	. . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
23	21, 22	eqtri 2190	. . . . . 6 |- (_i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
24	23	breq2i 3547	. . . . 5 |- (A~PRR(_i` 1) <-> A~PRRU.{y | (<.0R, 1R>."{1}) = {y}})
25		df-r 6839	. . . . . . 7 |- RR = (R. X. {0R})
26		sseq2 2898	. . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z C_ RR <-> z C_ (R. X. {0R})))
27	26	abbidv 2286	. . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z C_ RR} = {z | z C_ (R. X. {0R})})
28		df-pw 3261	. . . . . . . 8 |- ~PRR = {z | z C_ RR}
29		df-pw 3261	. . . . . . . 8 |- ~P(R. X. {0R}) = {z | z C_ (R. X. {0R})}
30	27, 28, 29	3eqtr4g 2230	. . . . . . 7 |- (RR = (R. X. {0R}) -> ~PRR = ~P(R. X. {0R}))
31	25, 30	ax-mp 7	. . . . . 6 |- ~PRR = ~P(R. X. {0R})
32	31	breqi 3545	. . . . 5 |- (A~PRRU.{y | (<.0R, 1R>."{1}) = {y}} <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
33	24, 32	bitri 306	. . . 4 |- (A~PRR(_i` 1) <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
34	33	anbi1i 805	. . 3 |- ((A~PRR(_i` 1) /\ F(/)(0 x. 1)) <-> (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1)))
35	34	notbii 362	. 2 |- (-. (A~PRR(_i` 1) /\ F(/)(0 x. 1)) <-> -. (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1)))
36	19, 35	mpbir 255	1 |- -. (A~PRR(_i` 1) /\ F(/)(0 x. 1))

Syntax hints:  -. wn 2   /\ wa 433   = wceq 1615   e. wcel 1617  {cab 2157  _Vcvv 2569   C_ wss 2859  (/)c0 3114  ~Pcpw 3259  {csn 3270  <.cop 3272  U.cuni 3398   class class class wbr 3539   X. cxp 4149  "cima 4154  ` cfv 4163  (class class class)co 5020  R.cnr 6588  0Rc0r 6589  1Rc1r 6590  RRcr 6828  0cc0 6829  1c1 6830  _ici 6831   x. cmul 6834

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-mulcl 6891  ax-mulcom 6893  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1rid 6899  ax-cnre 6902

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-xp 4165  df-cnv 4167  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fv 4179  df-opr 5022  df-i 6838  df-r 6839

Copyright terms: Public domain