Theorem avril1 9042

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	|- -. (AP~RR(i` 1) /\ F(/)(0 x. 1))

Proof of Theorem avril1

Step	Hyp	Ref	Expression
1		equid 1159	. . . . . . . 8 |- x = x
2		dfnul2 2332	. . . . . . . . . 10 |- (/) = {x | -. x = x}
3	2	abeq2i 1611	. . . . . . . . 9 |- (x e. (/) <-> -. x = x)
4	3	con2bii 219	. . . . . . . 8 |- (x = x <-> -. x e. (/))
5	1, 4	mpbi 187	. . . . . . 7 |- -. x e. (/)
6		eleq1 1575	. . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
7	5, 6	mtbii 719	. . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
8	7	vtocleg 1899	. . . . 5 |- (<.F, 0>. e. V -> -. <.F, 0>. e. (/))
9		elisset 1861	. . . . . 6 |- (<.F, 0>. e. (/) -> <.F, 0>. e. V)
10	9	con3i 98	. . . . 5 |- (-. <.F, 0>. e. V -> -. <.F, 0>. e. (/))
11	8, 10	pm2.61i 124	. . . 4 |- -. <.F, 0>. e. (/)
12		df-br 2688	. . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13		0cn 5479	. . . . . . . 8 |- 0 e. CC
14	13	mulid1i 5483	. . . . . . 7 |- (0 x. 1) = 0
15	14	opeq2i 2551	. . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
16	15	eleq1i 1578	. . . . 5 |- (<.F, (0 x. 1)>. e. (/) <-> <.F, 0>. e. (/))
17	12, 16	bitri 171	. . . 4 |- (F(/)(0 x. 1) <-> <.F, 0>. e. (/))
18	11, 17	mtbir 190	. . 3 |- -. F(/)(0 x. 1)
19	18	intnan 694	. 2 |- -. (AP~(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1))
20		df-i 5394	. . . . . . . 8 |- i = <.0R, 1R>.
21	20	fveq1i 3834	. . . . . . 7 |- (i` 1) = (<.0R, 1R>.` 1)
22		df-fv 3278	. . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
23	21, 22	eqtri 1536	. . . . . 6 |- (i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
24	23	breq2i 2695	. . . . 5 |- (AP~RR(i` 1) <-> AP~RRU.{y | (<.0R, 1R>."{1}) = {y}})
25		df-r 5395	. . . . . . 7 |- RR = (R. X. {0R})
26		sseq2 2133	. . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z (_ RR <-> z (_ (R. X. {0R})))
27	26	abbidv 1618	. . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z (_ RR} = {z | z (_ (R. X. {0R})})
28		df-pw 2454	. . . . . . . 8 |- P~RR = {z | z (_ RR}
29		df-pw 2454	. . . . . . . 8 |- P~(R. X. {0R}) = {z | z (_ (R. X. {0R})}
30	27, 28, 29	3eqtr4g 1572	. . . . . . 7 |- (RR = (R. X. {0R}) -> P~RR = P~(R. X. {0R}))
31	25, 30	ax-mp 7	. . . . . 6 |- P~RR = P~(R. X. {0R})
32	31	breqi 2693	. . . . 5 |- (AP~RRU.{y | (<.0R, 1R>."{1}) = {y}} <-> AP~(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
33	24, 32	bitri 171	. . . 4 |- (AP~RR(i` 1) <-> AP~(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
34	33	anbi1i 483	. . 3 |- ((AP~RR(i` 1) /\ F(/)(0 x. 1)) <-> (AP~(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1)))
35	34	notbii 185	. 2 |- (-. (AP~RR(i` 1) /\ F(/)(0 x. 1)) <-> -. (AP~(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1)))
36	19, 35	mpbir 188	1 |- -. (AP~RR(i` 1) /\ F(/)(0 x. 1))

Syntax hints:  -. wn 2   /\ wa 221   = wceq 989   e. wcel 991  {cab 1503  Vcvv 1855   (_ wss 2097  (/)c0 2330  P~cpw 2453  {csn 2462  <.cop 2464  U.cuni 2564   class class class wbr 2687   X. cxp 3248  "cima 3253  ` cfv 3262  (class class class)co 4018  R.cnr 5144  0Rc0r 5145  1Rc1r 5146  RRcr 5384  0cc0 5385  1c1 5386  ici 5387   x. cmul 5390

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 995  ax-gen 996  ax-8 997  ax-9 998  ax-10 999  ax-11 1000  ax-12 1001  ax-13 1002  ax-14 1003  ax-17 1004  ax-4 1006  ax-5o 1008  ax-6o 1011  ax-9o 1156  ax-10o 1174  ax-16 1244  ax-11o 1252  ax-ext 1498  ax-rep 2763  ax-sep 2773  ax-nul 2780  ax-pow 2814  ax-pr 2853  ax-un 3088  ax-inf2 4767

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 779  df-3an 780  df-ex 1014  df-sb 1206  df-eu 1419  df-mo 1420  df-clab 1504  df-cleq 1509  df-clel 1512  df-ne 1628  df-ral 1693  df-rex 1694  df-reu 1695  df-rab 1696  df-v 1856  df-sbc 1985  df-csb 2050  df-dif 2099  df-un 2100  df-in 2101  df-ss 2103  df-pss 2105  df-nul 2331  df-if 2414  df-pw 2454  df-sn 2465  df-pr 2466  df-tp 2468  df-op 2469  df-uni 2565  df-int 2596  df-iun 2630  df-br 2688  df-opab 2736  df-tr 2750  df-eprel 2908  df-id 2911  df-po 2916  df-so 2928  df-fr 2946  df-we 2961  df-ord 2977  df-on 2978  df-lim 2979  df-suc 2980  df-om 3218  df-xp 3264  df-rel 3265  df-cnv 3266  df-co 3267  df-dm 3268  df-rn 3269  df-res 3270  df-ima 3271  df-fun 3272  df-fn 3273  df-f 3274  df-fv 3278  df-opr 4020  df-oprab 4021  df-1st 4137  df-2nd 4138  df-rdg 4230  df-1o 4266  df-oadd 4268  df-omul 4269  df-er 4398  df-ec 4400  df-qs 4403  df-ni 5151  df-pli 5152  df-mi 5153  df-lti 5154  df-plpq 5186  df-mpq 5187  df-enq 5188  df-nq 5189  df-plq 5190  df-mq 5191  df-rq 5192  df-ltq 5193  df-1q 5194  df-np 5237  df-1p 5238  df-plp 5239  df-mp 5240  df-ltp 5241  df-plpr 5315  df-mpr 5316  df-enr 5317  df-nr 5318  df-plr 5319  df-mr 5320  df-0r 5322  df-1r 5323  df-m1r 5324  df-c 5391  df-0 5392  df-1 5393  df-i 5394  df-r 5395  df-plus 5396  df-mul 5397

Copyright terms: Public domain