Theorem avril1 9052

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 1161	. . . . . . . 8 |- x = x
2		dfnul2 2333	. . . . . . . . . 10 |- (/) = {x | -. x = x}
3	2	abeq2i 1612	. . . . . . . . 9 |- (x e. (/) <-> -. x = x)
4	3	con2bii 219	. . . . . . . 8 |- (x = x <-> -. x e. (/))
5	1, 4	mpbi 187	. . . . . . 7 |- -. x e. (/)
6		eleq1 1576	. . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
7	5, 6	mtbii 720	. . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
8	7	vtocleg 1900	. . . . 5 |- (<.F, 0>. e. V -> -. <.F, 0>. e. (/))
9		elisset 1862	. . . . . 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 2692	. . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13		0cn 5480	. . . . . . . 8 |- 0 e. CC
14	13	mulid1i 5484	. . . . . . 7 |- (0 x. 1) = 0
15	14	opeq2i 2555	. . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
16	15	eleq1i 1579	. . . . 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 5395	. . . . . . . 8 |- i = <.0R, 1R>.
21	20	fveq1i 3835	. . . . . . 7 |- (i` 1) = (<.0R, 1R>.` 1)
22		df-fv 3278	. . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
23	21, 22	eqtri 1537	. . . . . 6 |- (i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
24	23	breq2i 2699	. . . . 5 |- (AP~RR(i` 1) <-> AP~RRU.{y | (<.0R, 1R>."{1}) = {y}})
25		df-r 5396	. . . . . . 7 |- RR = (R. X. {0R})
26		sseq2 2134	. . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z (_ RR <-> z (_ (R. X. {0R})))
27	26	abbidv 1619	. . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z (_ RR} = {z | z (_ (R. X. {0R})})
28		df-pw 2458	. . . . . . . 8 |- P~RR = {z | z (_ RR}
29		df-pw 2458	. . . . . . . 8 |- P~(R. X. {0R}) = {z | z (_ (R. X. {0R})}
30	27, 28, 29	3eqtr4g 1573	. . . . . . 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 2697	. . . . 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 991   e. wcel 993  {cab 1504  Vcvv 1856   (_ wss 2098  (/)c0 2331  P~cpw 2457  {csn 2466  <.cop 2468  U.cuni 2568   class class class wbr 2691   X. cxp 3248  "cima 3253  ` cfv 3262  (class class class)co 4019  R.cnr 5145  0Rc0r 5146  1Rc1r 5147  RRcr 5385  0cc0 5386  1c1 5387  ici 5388   x. cmul 5391

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 997  ax-gen 998  ax-8 999  ax-9 1000  ax-10 1001  ax-11 1002  ax-12 1003  ax-13 1004  ax-14 1005  ax-17 1006  ax-4 1008  ax-5o 1010  ax-6o 1013  ax-9o 1158  ax-10o 1176  ax-16 1246  ax-11o 1254  ax-ext 1499  ax-rep 2766  ax-sep 2776  ax-nul 2783  ax-pow 2817  ax-pr 2854  ax-un 3088  ax-inf2 4768

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 781  df-3an 782  df-ex 1016  df-sb 1208  df-eu 1420  df-mo 1421  df-clab 1505  df-cleq 1510  df-clel 1513  df-ne 1629  df-ral 1694  df-rex 1695  df-reu 1696  df-rab 1697  df-v 1857  df-sbc 1986  df-csb 2051  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2415  df-pw 2458  df-sn 2469  df-pr 2470  df-tp 2472  df-op 2473  df-uni 2569  df-int 2600  df-iun 2634  df-br 2692  df-opab 2740  df-tr 2754  df-eprel 2909  df-id 2912  df-po 2917  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 4021  df-oprab 4022  df-1st 4138  df-2nd 4139  df-rdg 4231  df-1o 4267  df-oadd 4269  df-omul 4270  df-er 4399  df-ec 4401  df-qs 4404  df-ni 5152  df-pli 5153  df-mi 5154  df-lti 5155  df-plpq 5187  df-mpq 5188  df-enq 5189  df-nq 5190  df-plq 5191  df-mq 5192  df-rq 5193  df-ltq 5194  df-1q 5195  df-np 5238  df-1p 5239  df-plp 5240  df-mp 5241  df-ltp 5242  df-plpr 5316  df-mpr 5317  df-enr 5318  df-nr 5319  df-plr 5320  df-mr 5321  df-0r 5323  df-1r 5324  df-m1r 5325  df-c 5392  df-0 5393  df-1 5394  df-i 5395  df-r 5396  df-plus 5397  df-mul 5398

Copyright terms: Public domain