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

Theorem avril1 28252
 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 2019 . . . . . . . 8 𝑥 = 𝑥
2 dfnul2 4248 . . . . . . . . . 10 ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
32abeq2i 2928 . . . . . . . . 9 (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
43con2bii 361 . . . . . . . 8 (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅)
51, 4mpbi 233 . . . . . . 7 ¬ 𝑥 ∈ ∅
6 eleq1 2880 . . . . . . 7 (𝑥 = ⟨𝐹, 0⟩ → (𝑥 ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅))
75, 6mtbii 329 . . . . . 6 (𝑥 = ⟨𝐹, 0⟩ → ¬ ⟨𝐹, 0⟩ ∈ ∅)
87vtocleg 3532 . . . . 5 (⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
9 elex 3462 . . . . . 6 (⟨𝐹, 0⟩ ∈ ∅ → ⟨𝐹, 0⟩ ∈ V)
109con3i 157 . . . . 5 (¬ ⟨𝐹, 0⟩ ∈ V → ¬ ⟨𝐹, 0⟩ ∈ ∅)
118, 10pm2.61i 185 . . . 4 ¬ ⟨𝐹, 0⟩ ∈ ∅
12 df-br 5034 . . . . 5 (𝐹∅(0 · 1) ↔ ⟨𝐹, (0 · 1)⟩ ∈ ∅)
13 0cn 10626 . . . . . . . 8 0 ∈ ℂ
1413mulid1i 10638 . . . . . . 7 (0 · 1) = 0
1514opeq2i 4772 . . . . . 6 𝐹, (0 · 1)⟩ = ⟨𝐹, 0⟩
1615eleq1i 2883 . . . . 5 (⟨𝐹, (0 · 1)⟩ ∈ ∅ ↔ ⟨𝐹, 0⟩ ∈ ∅)
1712, 16bitri 278 . . . 4 (𝐹∅(0 · 1) ↔ ⟨𝐹, 0⟩ ∈ ∅)
1811, 17mtbir 326 . . 3 ¬ 𝐹∅(0 · 1)
1918intnan 490 . 2 ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1))
20 df-i 10539 . . . . . . . 8 i = ⟨0R, 1R
2120fveq1i 6650 . . . . . . 7 (i‘1) = (⟨0R, 1R⟩‘1)
22 df-fv 6336 . . . . . . 7 (⟨0R, 1R⟩‘1) = (℩𝑦1⟨0R, 1R𝑦)
2321, 22eqtri 2824 . . . . . 6 (i‘1) = (℩𝑦1⟨0R, 1R𝑦)
2423breq2i 5041 . . . . 5 (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R𝑦))
25 df-r 10540 . . . . . . 7 ℝ = (R × {0R})
26 sseq2 3944 . . . . . . . . 9 (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R})))
2726abbidv 2865 . . . . . . . 8 (ℝ = (R × {0R}) → {𝑧𝑧 ⊆ ℝ} = {𝑧𝑧 ⊆ (R × {0R})})
28 df-pw 4502 . . . . . . . 8 𝒫 ℝ = {𝑧𝑧 ⊆ ℝ}
29 df-pw 4502 . . . . . . . 8 𝒫 (R × {0R}) = {𝑧𝑧 ⊆ (R × {0R})}
3027, 28, 293eqtr4g 2861 . . . . . . 7 (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R}))
3125, 30ax-mp 5 . . . . . 6 𝒫 ℝ = 𝒫 (R × {0R})
3231breqi 5039 . . . . 5 (𝐴𝒫 ℝ(℩𝑦1⟨0R, 1R𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦))
3324, 32bitri 278 . . . 4 (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦))
3433anbi1i 626 . . 3 ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1)))
3534notbii 323 . 2 (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1⟨0R, 1R𝑦) ∧ 𝐹∅(0 · 1)))
3619, 35mpbir 234 1 ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 399   = wceq 1538   ∈ wcel 2112  {cab 2779  Vcvv 3444   ⊆ wss 3884  ∅c0 4246  𝒫 cpw 4500  {csn 4528  ⟨cop 4534   class class class wbr 5033   × cxp 5521  ℩cio 6285  ‘cfv 6328  (class class class)co 7139  Rcnr 10280  0Rc0r 10281  1Rc1r 10282  ℝcr 10529  0cc0 10530  1c1 10531  ici 10532   · cmul 10535 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-12 2176  ax-ext 2773  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-mulcl 10592  ax-mulcom 10594  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1rid 10600  ax-cnre 10603 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-i 10539  df-r 10540 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator