Theorem avril1 29305

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 2015	. . . . . . . 8 ⊢ 𝑥 = 𝑥
2		dfnul2 4284	. . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
3	2	abeq2i 2879	. . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
4	3	con2bii 357	. . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
5	1, 4	mpbi 229	. . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅
6		eleq1 2825	. . . . . . 7 ⊢ (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
7	5, 6	mtbii 325	. . . . . 6 ⊢ (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
8	7	vtocleg 3513	. . . . 5 ⊢ (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9		elex 3462	. . . . . 6 ⊢ (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
10	9	con3i 154	. . . . 5 ⊢ (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
11	8, 10	pm2.61i 182	. . . 4 ⊢ ¬ ⟨𝐹, 0⟩ ∈ ∅
12		df-br 5105	. . . . 5 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13		0cn 11144	. . . . . . . 8 ⊢ 0 ∈ ℂ
14	13	mulid1i 11156	. . . . . . 7 ⊢ (0 · 1) = 0
15	14	opeq2i 4833	. . . . . 6 ⊢ ⟨𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
16	15	eleq1i 2828	. . . . 5 ⊢ (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
17	12, 16	bitri 274	. . . 4 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
18	11, 17	mtbir 322	. . 3 ⊢ ¬ 𝐹∅(0 · 1)
19	18	intnan 487	. 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1))
20		df-i 11057	. . . . . . . 8 ⊢ i = ⟨0R, 1R⟩
21	20	fveq1i 6841	. . . . . . 7 ⊢ (i‘1) = (⟨0R, 1R⟩‘1)
22		df-fv 6502	. . . . . . 7 ⊢ (⟨0R, 1R⟩‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
23	21, 22	eqtri 2764	. . . . . 6 ⊢ (i‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
24	23	breq2i 5112	. . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦))
25		df-r 11058	. . . . . . 7 ⊢ ℝ = (R × {0R})
26		sseq2 3969	. . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
27	26	abbidv 2805	. . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})})
28		df-pw 4561	. . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ}
29		df-pw 4561	. . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}
30	27, 28, 29	3eqtr4g 2801	. . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
31	25, 30	ax-mp 5	. . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R})
32	31	breqi 5110	. . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
33	24, 32	bitri 274	. . . 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 319	. 2 ⊢ (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
36	19, 35	mpbir 230	1 ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2713  Vcvv 3444   ⊆ wss 3909  ∅c0 4281  𝒫 cpw 4559  {csn 4585  ⟨cop 4591   class class class wbr 5104   × cxp 5630  ℩cio 6444  ‘cfv 6494  (class class class)co 7354  Rcnr 10798  0_Rc0r 10799  1_Rc1r 10800  ℝcr 11047  0cc0 11048  1c1 11049  ici 11050   · cmul 11053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2707  ax-resscn 11105  ax-1cn 11106  ax-icn 11107  ax-addcl 11108  ax-mulcl 11110  ax-mulcom 11112  ax-mulass 11114  ax-distr 11115  ax-i2m1 11116  ax-1rid 11118  ax-cnre 11121

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6446  df-fv 6502  df-ov 7357  df-i 11057  df-r 11058

This theorem is referenced by: (None)