MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  avril1 Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 equid 2015 . . . . . . . 8 𝑥 = 𝑥
2 dfnul2 4284 . . . . . . . . . 10 ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
32abeq2i 2879 . . . . . . . . 9 (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
43con2bii 357 . . . . . . . 8 (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
51, 4mpbi 229 . . . . . . 7 ¬ 𝑥 ∈ ∅
6 eleq1 2825 . . . . . . 7 (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
75, 6mtbii 325 . . . . . 6 (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
87vtocleg 3513 . . . . 5 (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9 elex 3462 . . . . . 6 (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
109con3i 154 . . . . 5 (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
118, 10pm2.61i 182 . . . 4 ¬ ⟨𝐹, 0⟩ ∈ ∅
12 df-br 5105 . . . . 5 (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13 0cn 11144 . . . . . . . 8 0 ∈ ℂ
1413mulid1i 11156 . . . . . . 7 (0 · 1) = 0
1514opeq2i 4833 . . . . . 6 𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
1615eleq1i 2828 . . . . 5 (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
1712, 16bitri 274 . . . 4 (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
1811, 17mtbir 322 . . 3 ¬ 𝐹∅(0 · 1)
1918intnan 487 . 2 ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1))
20 df-i 11057 . . . . . . . 8 i = ⟨0R, 1R
2120fveq1i 6841 . . . . . . 7 (i‘1) = (⟨0R, 1R⟩‘1)
22 df-fv 6502 . . . . . . 7 (⟨0R, 1R⟩‘1) = (℩𝑦1⟨0R, 1R𝑦)
2321, 22eqtri 2764 . . . . . 6 (i‘1) = (℩𝑦1⟨0R, 1R𝑦)
2423breq2i 5112 . . . . 5 (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R𝑦))
25 df-r 11058 . . . . . . 7 ℝ = (R × {0R})
26 sseq2 3969 . . . . . . . . 9 (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
2726abbidv 2805 . . . . . . . 8 (ℝ = (R × {0R}) → {𝑧𝑧 ⊆ ℝ} = {𝑧𝑧 ⊆ (R × {0R})})
28 df-pw 4561 . . . . . . . 8 𝒫 ℝ = {𝑧𝑧 ⊆ ℝ}
29 df-pw 4561 . . . . . . . 8 𝒫 (R × {0R}) = {𝑧𝑧 ⊆ (R × {0R})}
3027, 28, 293eqtr4g 2801 . . . . . . 7 (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
3125, 30ax-mp 5 . . . . . 6 𝒫 ℝ = 𝒫 (R × {0R})
3231breqi 5110 . . . . 5 (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦))
3324, 32bitri 274 . . . 4 (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦))
3433anbi1i 624 . . 3 ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1)))
3534notbii 319 . 2 (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1)))
3619, 35mpbir 230 1 ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))
Colors of variables: wff setvar class
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  0Rc0r 10799  1Rc1r 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)
  Copyright terms: Public domain W3C validator