Theorem avril1 27319

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 german 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.) (Proof modification is discouraged.) (New usage is discouraged.)

A reply to skeptics can be found at mmnotes.txt, under the 1-Apr-2006 entry.

Assertion

Ref	Expression
avril1	|- -. ( A ~P RR ( _i ` 1 ) /\ F (/) ( 0 x. 1 ) )

Proof of Theorem avril1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equid 1939	. . . . . . . 8 |- x = x
2		dfnul2 3917	. . . . . . . . . 10 |- (/) = { x | -. x = x }
3	2	abeq2i 2735	. . . . . . . . 9 |- ( x e. (/) <-> -. x = x )
4	3	con2bii 347	. . . . . . . 8 |- ( x = x <-> -. x e. (/) )
5	1, 4	mpbi 220	. . . . . . 7 |- -. x e. (/)
6		eleq1 2689	. . . . . . 7 |- ( x = <. F , 0 >. -> ( x e. (/) <-> <. F , 0 >. e. (/) ) )
7	5, 6	mtbii 316	. . . . . 6 |- ( x = <. F , 0 >. -> -. <. F , 0 >. e. (/) )
8	7	vtocleg 3279	. . . . 5 |- ( <. F , 0 >. e. _V -> -. <. F , 0 >. e. (/) )
9		elex 3212	. . . . . 6 |- ( <. F , 0 >. e. (/) -> <. F , 0 >. e. _V )
10	9	con3i 150	. . . . 5 |- ( -. <. F , 0 >. e. _V -> -. <. F , 0 >. e. (/) )
11	8, 10	pm2.61i 176	. . . 4 |- -. <. F , 0 >. e. (/)
12		df-br 4654	. . . . 5 |- ( F (/) ( 0 x. 1 ) <-> <. F , ( 0 x. 1 ) >. e. (/) )
13		0cn 10032	. . . . . . . 8 |- 0 e. CC
14	13	mulid1i 10042	. . . . . . 7 |- ( 0 x. 1 ) = 0
15	14	opeq2i 4406	. . . . . 6 |- <. F , ( 0 x. 1 ) >. = <. F , 0 >.
16	15	eleq1i 2692	. . . . 5 |- ( <. F , ( 0 x. 1 ) >. e. (/) <-> <. F , 0 >. e. (/) )
17	12, 16	bitri 264	. . . 4 |- ( F (/) ( 0 x. 1 ) <-> <. F , 0 >. e. (/) )
18	11, 17	mtbir 313	. . 3 |- -. F (/) ( 0 x. 1 )
19	18	intnan 960	. 2 |- -. ( A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) /\ F (/) ( 0 x. 1 ) )
20		df-i 9945	. . . . . . . 8 |- _i = <. 0R , 1R >.
21	20	fveq1i 6192	. . . . . . 7 |- ( _i ` 1 ) = ( <. 0R , 1R >. ` 1 )
22		df-fv 5896	. . . . . . 7 |- ( <. 0R , 1R >. ` 1 ) = ( iota y 1 <. 0R , 1R >. y )
23	21, 22	eqtri 2644	. . . . . 6 |- ( _i ` 1 ) = ( iota y 1 <. 0R , 1R >. y )
24	23	breq2i 4661	. . . . 5 |- ( A ~P RR ( _i ` 1 ) <-> A ~P RR ( iota y 1 <. 0R , 1R >. y ) )
25		df-r 9946	. . . . . . 7 |- RR = ( R. X. { 0R } )
26		sseq2 3627	. . . . . . . . 9 |- ( RR = ( R. X. { 0R } ) -> ( z C_ RR <-> z C_ ( R. X. { 0R } ) ) )
27	26	abbidv 2741	. . . . . . . 8 |- ( RR = ( R. X. { 0R } ) -> { z | z C_ RR } = { z | z C_ ( R. X. { 0R } ) } )
28		df-pw 4160	. . . . . . . 8 |- ~P RR = { z | z C_ RR }
29		df-pw 4160	. . . . . . . 8 |- ~P ( R. X. { 0R } ) = { z | z C_ ( R. X. { 0R } ) }
30	27, 28, 29	3eqtr4g 2681	. . . . . . 7 |- ( RR = ( R. X. { 0R } ) -> ~P RR = ~P ( R. X. { 0R } ) )
31	25, 30	ax-mp 5	. . . . . 6 |- ~P RR = ~P ( R. X. { 0R } )
32	31	breqi 4659	. . . . 5 |- ( A ~P RR ( iota y 1 <. 0R , 1R >. y ) <-> A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) )
33	24, 32	bitri 264	. . . 4 |- ( A ~P RR ( _i ` 1 ) <-> A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) )
34	33	anbi1i 731	. . 3 |- ( ( A ~P RR ( _i ` 1 ) /\ F (/) ( 0 x. 1 ) ) <-> ( A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) /\ F (/) ( 0 x. 1 ) ) )
35	34	notbii 310	. 2 |- ( -. ( A ~P RR ( _i ` 1 ) /\ F (/) ( 0 x. 1 ) ) <-> -. ( A ~P ( R. X. { 0R } ) ( iota y 1 <. 0R , 1R >. y ) /\ F (/) ( 0 x. 1 ) ) )
36	19, 35	mpbir 221	1 |- -. ( A ~P RR ( _i ` 1 ) /\ F (/) ( 0 x. 1 ) )

Syntax hints:   -. wn 3   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   _Vcvv 3200   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   <.cop 4183   class class class wbr 4653   X. cxp 5112   iotacio 5849   ` cfv 5888  (class class class)co 6650   R.cnr 9687   0Rc0r 9688   1Rc1r 9689   RRcr 9935   0cc0 9936   1c1 9937   _ici 9938   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulcom 10000  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1rid 10006  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-i 9945  df-r 9946

This theorem is referenced by: (None)