Theorem avril1 30622

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 2031	. . . . . . . 8 ⊢ 𝑥 = 𝑥
2		dfnul2 4286	. . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
3	2	eqabri 2903	. . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
4	3	con2bii 359	. . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
5	1, 4	mpbi 232	. . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅
6		eleq1 2849	. . . . . . 7 ⊢ (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
7	5, 6	mtbii 328	. . . . . 6 ⊢ (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
8	7	vtocleg 3520	. . . . 5 ⊢ (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9		elex 3474	. . . . . 6 ⊢ (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
10	9	con3i 154	. . . . 5 ⊢ (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
11	8, 10	pm2.61i 183	. . . 4 ⊢ ¬ ⟨𝐹, 0⟩ ∈ ∅
12		df-br 5098	. . . . 5 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13		0cn 11165	. . . . . . . 8 ⊢ 0 ∈ ℂ
14	13	mulridi 11180	. . . . . . 7 ⊢ (0 · 1) = 0
15	14	opeq2i 4832	. . . . . 6 ⊢ ⟨𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
16	15	eleq1i 2852	. . . . 5 ⊢ (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
17	12, 16	bitri 277	. . . 4 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
18	11, 17	mtbir 325	. . 3 ⊢ ¬ 𝐹∅(0 · 1)
19	18	intnan 490	. 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1))
20		df-i 11076	. . . . . . . 8 ⊢ i = ⟨0R, 1R⟩
21	20	fveq1i 6863	. . . . . . 7 ⊢ (i‘1) = (⟨0R, 1R⟩‘1)
22		df-fv 6524	. . . . . . 7 ⊢ (⟨0R, 1R⟩‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
23	21, 22	eqtri 2784	. . . . . 6 ⊢ (i‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
24	23	breq2i 5105	. . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦))
25		df-r 11077	. . . . . . 7 ⊢ ℝ = (R × {0R})
26		sseq2 3960	. . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
27	26	abbidv 2827	. . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})})
28		df-pw 4554	. . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ}
29		df-pw 4554	. . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}
30	27, 28, 29	3eqtr4g 2821	. . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
31	25, 30	ax-mp 5	. . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R})
32	31	breqi 5103	. . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
33	24, 32	bitri 277	. . . 4 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
34	33	anbi1i 633	. . 3 ⊢ ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
35	34	notbii 322	. 2 ⊢ (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
36	19, 35	mpbir 233	1 ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))

Syntax hints:  ¬ wn 3   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {cab 2739  Vcvv 3453   ⊆ wss 3902  ∅c0 4283  𝒫 cpw 4552  {csn 4579  ⟨cop 4585   class class class wbr 5097   × cxp 5641  ℩cio 6470  ‘cfv 6516  (class class class)co 7391  Rcnr 10817  0_Rc0r 10818  1_Rc1r 10819  ℝcr 11066  0cc0 11067  1c1 11068  ici 11069   · cmul 11072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-12 2211  ax-ext 2733  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-mulcl 11129  ax-mulcom 11131  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1rid 11137  ax-cnre 11140

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-i 11076  df-r 11077

This theorem is referenced by: (None)