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

Theorem avril1 27289
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 1937 . . . . . . . 8 𝑥 = 𝑥
2 dfnul2 3909 . . . . . . . . . 10 ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
32abeq2i 2733 . . . . . . . . 9 (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
43con2bii 347 . . . . . . . 8 (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
51, 4mpbi 220 . . . . . . 7 ¬ 𝑥 ∈ ∅
6 eleq1 2687 . . . . . . 7 (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
75, 6mtbii 316 . . . . . 6 (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
87vtocleg 3274 . . . . 5 (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9 elex 3207 . . . . . 6 (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
109con3i 150 . . . . 5 (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
118, 10pm2.61i 176 . . . 4 ¬ ⟨𝐹, 0⟩ ∈ ∅
12 df-br 4645 . . . . 5 (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13 0cn 10017 . . . . . . . 8 0 ∈ ℂ
1413mulid1i 10027 . . . . . . 7 (0 · 1) = 0
1514opeq2i 4397 . . . . . 6 𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
1615eleq1i 2690 . . . . 5 (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
1712, 16bitri 264 . . . 4 (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
1811, 17mtbir 313 . . 3 ¬ 𝐹∅(0 · 1)
1918intnan 959 . 2 ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1))
20 df-i 9930 . . . . . . . 8 i = ⟨0R, 1R
2120fveq1i 6179 . . . . . . 7 (i‘1) = (⟨0R, 1R⟩‘1)
22 df-fv 5884 . . . . . . 7 (⟨0R, 1R⟩‘1) = (℩𝑦1⟨0R, 1R𝑦)
2321, 22eqtri 2642 . . . . . 6 (i‘1) = (℩𝑦1⟨0R, 1R𝑦)
2423breq2i 4652 . . . . 5 (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R𝑦))
25 df-r 9931 . . . . . . 7 ℝ = (R × {0R})
26 sseq2 3619 . . . . . . . . 9 (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
2726abbidv 2739 . . . . . . . 8 (ℝ = (R × {0R}) → {𝑧𝑧 ⊆ ℝ} = {𝑧𝑧 ⊆ (R × {0R})})
28 df-pw 4151 . . . . . . . 8 𝒫 ℝ = {𝑧𝑧 ⊆ ℝ}
29 df-pw 4151 . . . . . . . 8 𝒫 (R × {0R}) = {𝑧𝑧 ⊆ (R × {0R})}
3027, 28, 293eqtr4g 2679 . . . . . . 7 (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
3125, 30ax-mp 5 . . . . . 6 𝒫 ℝ = 𝒫 (R × {0R})
3231breqi 4650 . . . . 5 (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦))
3324, 32bitri 264 . . . 4 (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦))
3433anbi1i 730 . . 3 ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1)))
3534notbii 310 . 2 (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1)))
3619, 35mpbir 221 1 ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 384   = wceq 1481  wcel 1988  {cab 2606  Vcvv 3195  wss 3567  c0 3907  𝒫 cpw 4149  {csn 4168  cop 4174   class class class wbr 4644   × cxp 5102  cio 5837  cfv 5876  (class class class)co 6635  Rcnr 9672  0Rc0r 9673  1Rc1r 9674  cr 9920  0cc0 9921  1c1 9922  ici 9923   · cmul 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-mulcl 9983  ax-mulcom 9985  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1rid 9991  ax-cnre 9994
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-i 9930  df-r 9931
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator