Theorem avril1 30558

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 2019	. . . . . . . 8 ⊢ 𝑥 = 𝑥
2		dfnul2 4271	. . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
3	2	eqabri 2882	. . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
4	3	con2bii 358	. . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
5	1, 4	mpbi 231	. . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅
6		eleq1 2828	. . . . . . 7 ⊢ (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
7	5, 6	mtbii 327	. . . . . 6 ⊢ (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
8	7	vtocleg 3501	. . . . 5 ⊢ (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9		elex 3453	. . . . . 6 ⊢ (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
10	9	con3i 154	. . . . 5 ⊢ (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
11	8, 10	pm2.61i 183	. . . 4 ⊢ ¬ ⟨𝐹, 0⟩ ∈ ∅
12		df-br 5080	. . . . 5 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13		0cn 11134	. . . . . . . 8 ⊢ 0 ∈ ℂ
14	13	mulridi 11147	. . . . . . 7 ⊢ (0 · 1) = 0
15	14	opeq2i 4815	. . . . . 6 ⊢ ⟨𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
16	15	eleq1i 2831	. . . . 5 ⊢ (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
17	12, 16	bitri 276	. . . 4 ⊢ (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
18	11, 17	mtbir 324	. . 3 ⊢ ¬ 𝐹∅(0 · 1)
19	18	intnan 487	. 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1))
20		df-i 11045	. . . . . . . 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 2763	. . . . . 6 ⊢ (i‘1) = (℩𝑦1⟨0R, 1R⟩𝑦)
24	23	breq2i 5087	. . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦))
25		df-r 11046	. . . . . . 7 ⊢ ℝ = (R × {0R})
26		sseq2 3948	. . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
27	26	abbidv 2806	. . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})})
28		df-pw 4538	. . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ}
29		df-pw 4538	. . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}
30	27, 28, 29	3eqtr4g 2800	. . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
31	25, 30	ax-mp 5	. . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R})
32	31	breqi 5085	. . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R⟩𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
33	24, 32	bitri 276	. . . 4 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦))
34	33	anbi1i 630	. . 3 ⊢ ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
35	34	notbii 321	. 2 ⊢ (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R⟩𝑦) ∧ 𝐹∅(0 · 1)))
36	19, 35	mpbir 232	1 ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2718  Vcvv 3432   ⊆ wss 3890  ∅c0 4268  𝒫 cpw 4536  {csn 4562  ⟨cop 4568   class class class wbr 5079   × cxp 5623  ℩cio 6446  ‘cfv 6492  (class class class)co 7363  Rcnr 10786  0_Rc0r 10787  1_Rc1r 10788  ℝcr 11035  0cc0 11036  1c1 11037  ici 11038   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2712  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-mulcom 11100  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1rid 11106  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-i 11045  df-r 11046

This theorem is referenced by: (None)