Theorem avril1 30538

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 𝑥 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	⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))

Proof of Theorem avril1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equid 2013	. . . . . . . 8 ⊢ 𝑥 = 𝑥
2		dfnul2 4288	. . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
3	2	eqabri 2878	. . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
4	3	con2bii 357	. . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
5	1, 4	mpbi 230	. . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅
6		eleq1 2824	. . . . . . 7 ⊢ (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
7	5, 6	mtbii 326	. . . . . 6 ⊢ (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
8	7	vtocleg 3510	. . . . 5 ⊢ (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9		elex 3461	. . . . . 6 ⊢ (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
10	9	con3i 154	. . . . 5 ⊢ (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
11	8, 10	pm2.61i 182	. . . 4 ⊢ ¬ ⟨𝐹, 0⟩ ∈ ∅
12		df-br 5099	. . . . 5 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13		0cn 11124	. . . . . . . 8 ⊢ 0 ∈ ℂ
14	13	mulridi 11136	. . . . . . 7 ⊢ (0 · 1) = 0
15	14	opeq2i 4833	. . . . . 6 ⊢ ⟨𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
16	15	eleq1i 2827	. . . . 5 ⊢ (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
17	12, 16	bitri 275	. . . 4 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
18	11, 17	mtbir 323	. . 3 ⊢ ¬ 𝐹∅(0 · 1)
19	18	intnan 486	. 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1))
20		df-i 11035	. . . . . . . 8 ⊢ i = ⟨0R, 1R⟩
21	20	fveq1i 6835	. . . . . . 7 ⊢ (i‘1) = (⟨0R, 1R⟩‘1)
22		df-fv 6500	. . . . . . 7 ⊢ (⟨0R, 1R⟩‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
23	21, 22	eqtri 2759	. . . . . 6 ⊢ (i‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
24	23	breq2i 5106	. . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦))
25		df-r 11036	. . . . . . 7 ⊢ ℝ = (R × {0R})
26		sseq2 3960	. . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
27	26	abbidv 2802	. . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})})
28		df-pw 4556	. . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ}
29		df-pw 4556	. . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}
30	27, 28, 29	3eqtr4g 2796	. . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
31	25, 30	ax-mp 5	. . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R})
32	31	breqi 5104	. . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
33	24, 32	bitri 275	. . . 4 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
34	33	anbi1i 624	. . 3 ⊢ ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
35	34	notbii 320	. 2 ⊢ (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
36	19, 35	mpbir 231	1 ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2714  Vcvv 3440   ⊆ wss 3901  ∅c0 4285  𝒫 cpw 4554  {csn 4580  ⟨cop 4586   class class class wbr 5098   × cxp 5622  ℩cio 6446  ‘cfv 6492  (class class class)co 7358  Rcnr 10776  0_Rc0r 10777  1_Rc1r 10778  ℝcr 11025  0cc0 11026  1c1 11027  ici 11028   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2184  ax-ext 2708  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulcom 11090  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1rid 11096  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-i 11035  df-r 11036

This theorem is referenced by: (None)