Theorem avril1 9035

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 5473	. . . . . . . 8 |- 0 e. CC
14	13	mulid1i 5477	. . . . . . 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 5388	. . . . . . . 8 |- i = <.0R, 1R>.
21	20	fveq1i 3832	. . . . . . 7 |- (i` 1) = (<.0R, 1R>.` 1)
22		df-fv 3276	. . . . . . 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 5389	. . . . . . 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 3246  "cima 3251  ` cfv 3260  (class class class)co 4016  R.cnr 5138  0Rc0r 5139  1Rc1r 5140  RRcr 5378  0cc0 5379  1c1 5380  ici 5381   x. cmul 5384

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 2813  ax-pr 2851  ax-un 3086  ax-inf2 4761

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 2906  df-id 2909  df-po 2914  df-so 2926  df-fr 2944  df-we 2959  df-ord 2975  df-on 2976  df-lim 2977  df-suc 2978  df-om 3216  df-xp 3262  df-rel 3263  df-cnv 3264  df-co 3265  df-dm 3266  df-rn 3267  df-res 3268  df-ima 3269  df-fun 3270  df-fn 3271  df-f 3272  df-fv 3276  df-opr 4018  df-oprab 4019  df-1st 4135  df-2nd 4136  df-rdg 4228  df-1o 4264  df-oadd 4266  df-omul 4267  df-er 4396  df-ec 4398  df-qs 4401  df-ni 5145  df-pli 5146  df-mi 5147  df-lti 5148  df-plpq 5180  df-mpq 5181  df-enq 5182  df-nq 5183  df-plq 5184  df-mq 5185  df-rq 5186  df-ltq 5187  df-1q 5188  df-np 5231  df-1p 5232  df-plp 5233  df-mp 5234  df-ltp 5235  df-plpr 5309  df-mpr 5310  df-enr 5311  df-nr 5312  df-plr 5313  df-mr 5314  df-0r 5316  df-1r 5317  df-m1r 5318  df-c 5385  df-0 5386  df-1 5387  df-i 5388  df-r 5389  df-plus 5390  df-mul 5391

Copyright terms: Public domain