Theorem avril1 31121

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 2047	. . . . . . . 8 ⊢ 𝑥 = 𝑥
2		dfnul2 4284	. . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
3	2	eqabri 2906	. . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
4	3	con2bii 360	. . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
5	1, 4	mpbi 233	. . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅
6		eleq1 2852	. . . . . . 7 ⊢ (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
7	5, 6	mtbii 329	. . . . . 6 ⊢ (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
8	7	vtocleg 3520	. . . . 5 ⊢ (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9		elex 3475	. . . . . 6 ⊢ (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
10	9	con3i 155	. . . . 5 ⊢ (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
11	8, 10	pm2.61i 184	. . . 4 ⊢ ¬ ⟨𝐹, 0⟩ ∈ ∅
12		df-br 5109	. . . . 5 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13		0cn 11337	. . . . . . . 8 ⊢ 0 ∈ ℂ
14	13	mulridi 11352	. . . . . . 7 ⊢ (0 · 1) = 0
15	14	opeq2i 4849	. . . . . 6 ⊢ ⟨𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
16	15	eleq1i 2855	. . . . 5 ⊢ (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
17	12, 16	bitri 278	. . . 4 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
18	11, 17	mtbir 326	. . 3 ⊢ ¬ 𝐹∅(0 · 1)
19	18	intnan 492	. 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1))
20		df-i 11248	. . . . . . . 8 ⊢ i = ⟨0R, 1R⟩
21	20	fveq1i 6917	. . . . . . 7 ⊢ (i‘1) = (⟨0R, 1R⟩‘1)
22		df-fv 6574	. . . . . . 7 ⊢ (⟨0R, 1R⟩‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
23	21, 22	eqtri 2786	. . . . . 6 ⊢ (i‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
24	23	breq2i 5116	. . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦))
25		df-r 11249	. . . . . . 7 ⊢ ℝ = (R × {0R})
26		sseq2 3939	. . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
27	26	abbidv 2829	. . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})})
28		df-pw 4562	. . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ}
29		df-pw 4562	. . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}
30	27, 28, 29	3eqtr4g 2823	. . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
31	25, 30	ax-mp 5	. . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R})
32	31	breqi 5114	. . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
33	24, 32	bitri 278	. . . 4 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
34	33	anbi1i 636	. . 3 ⊢ ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
35	34	notbii 323	. 2 ⊢ (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
36	19, 35	mpbir 234	1 ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {cab 2741  Vcvv 3454   ⊆ wss 3900  ∅c0 4281  𝒫 cpw 4560  {csn 4588  ⟨cop 4840   class class class wbr 5108   × cxp 5656  ℩cio 6518  ‘cfv 6566  (class class class)co 7451  Rcnr 10989  0_Rc0r 10990  1_Rc1r 10991  ℝcr 11238  0cc0 11239  1c1 11240  ici 11241   · cmul 11244

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-mulcom 11303  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1rid 11309  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-i 11248  df-r 11249

This theorem is used by: (None)