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

Theorem avril1 27655
 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 2096 . . . . . . . 8 𝑥 = 𝑥
2 dfnul2 4063 . . . . . . . . . 10 ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
32abeq2i 2883 . . . . . . . . 9 (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
43con2bii 346 . . . . . . . 8 (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
51, 4mpbi 220 . . . . . . 7 ¬ 𝑥 ∈ ∅
6 eleq1 2837 . . . . . . 7 (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
75, 6mtbii 315 . . . . . 6 (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
87vtocleg 3428 . . . . 5 (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9 elex 3361 . . . . . 6 (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
109con3i 151 . . . . 5 (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
118, 10pm2.61i 176 . . . 4 ¬ ⟨𝐹, 0⟩ ∈ ∅
12 df-br 4785 . . . . 5 (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13 0cn 10233 . . . . . . . 8 0 ∈ ℂ
1413mulid1i 10243 . . . . . . 7 (0 · 1) = 0
1514opeq2i 4541 . . . . . 6 𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
1615eleq1i 2840 . . . . 5 (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
1712, 16bitri 264 . . . 4 (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
1811, 17mtbir 312 . . 3 ¬ 𝐹∅(0 · 1)
1918intnan 996 . 2 ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1))
20 df-i 10146 . . . . . . . 8 i = ⟨0R, 1R
2120fveq1i 6333 . . . . . . 7 (i‘1) = (⟨0R, 1R⟩‘1)
22 df-fv 6039 . . . . . . 7 (⟨0R, 1R⟩‘1) = (℩𝑦1⟨0R, 1R𝑦)
2321, 22eqtri 2792 . . . . . 6 (i‘1) = (℩𝑦1⟨0R, 1R𝑦)
2423breq2i 4792 . . . . 5 (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R𝑦))
25 df-r 10147 . . . . . . 7 ℝ = (R × {0R})
26 sseq2 3774 . . . . . . . . 9 (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
2726abbidv 2889 . . . . . . . 8 (ℝ = (R × {0R}) → {𝑧𝑧 ⊆ ℝ} = {𝑧𝑧 ⊆ (R × {0R})})
28 df-pw 4297 . . . . . . . 8 𝒫 ℝ = {𝑧𝑧 ⊆ ℝ}
29 df-pw 4297 . . . . . . . 8 𝒫 (R × {0R}) = {𝑧𝑧 ⊆ (R × {0R})}
3027, 28, 293eqtr4g 2829 . . . . . . 7 (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
3125, 30ax-mp 5 . . . . . 6 𝒫 ℝ = 𝒫 (R × {0R})
3231breqi 4790 . . . . 5 (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦))
3324, 32bitri 264 . . . 4 (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦))
3433anbi1i 602 . . 3 ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1)))
3534notbii 309 . 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 382   = wceq 1630   ∈ wcel 2144  {cab 2756  Vcvv 3349   ⊆ wss 3721  ∅c0 4061  𝒫 cpw 4295  {csn 4314  ⟨cop 4320   class class class wbr 4784   × cxp 5247  ℩cio 5992  ‘cfv 6031  (class class class)co 6792  Rcnr 9888  0Rc0r 9889  1Rc1r 9890  ℝcr 10136  0cc0 10137  1c1 10138  ici 10139   · cmul 10142 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-mulcl 10199  ax-mulcom 10201  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1rid 10207  ax-cnre 10210 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-ov 6795  df-i 10146  df-r 10147 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator