Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > avril1 | Structured version Visualization version GIF version |
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. |
Ref | Expression |
---|---|
avril1 | ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equid 2022 | . . . . . . . 8 ⊢ 𝑥 = 𝑥 | |
2 | dfnul2 4226 | . . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | |
3 | 2 | abeq2i 2865 | . . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥) |
4 | 3 | con2bii 361 | . . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅) |
5 | 1, 4 | mpbi 233 | . . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅ |
6 | eleq1 2818 | . . . . . . 7 ⊢ (𝑥 = 〈𝐹, 0〉 → (𝑥 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅)) | |
7 | 5, 6 | mtbii 329 | . . . . . 6 ⊢ (𝑥 = 〈𝐹, 0〉 → ¬ 〈𝐹, 0〉 ∈ ∅) |
8 | 7 | vtocleg 3487 | . . . . 5 ⊢ (〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
9 | elex 3416 | . . . . . 6 ⊢ (〈𝐹, 0〉 ∈ ∅ → 〈𝐹, 0〉 ∈ V) | |
10 | 9 | con3i 157 | . . . . 5 ⊢ (¬ 〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
11 | 8, 10 | pm2.61i 185 | . . . 4 ⊢ ¬ 〈𝐹, 0〉 ∈ ∅ |
12 | df-br 5040 | . . . . 5 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, (0 · 1)〉 ∈ ∅) | |
13 | 0cn 10790 | . . . . . . . 8 ⊢ 0 ∈ ℂ | |
14 | 13 | mulid1i 10802 | . . . . . . 7 ⊢ (0 · 1) = 0 |
15 | 14 | opeq2i 4774 | . . . . . 6 ⊢ 〈𝐹, (0 · 1)〉 = 〈𝐹, 0〉 |
16 | 15 | eleq1i 2821 | . . . . 5 ⊢ (〈𝐹, (0 · 1)〉 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅) |
17 | 12, 16 | bitri 278 | . . . 4 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, 0〉 ∈ ∅) |
18 | 11, 17 | mtbir 326 | . . 3 ⊢ ¬ 𝐹∅(0 · 1) |
19 | 18 | intnan 490 | . 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1)) |
20 | df-i 10703 | . . . . . . . 8 ⊢ i = 〈0R, 1R〉 | |
21 | 20 | fveq1i 6696 | . . . . . . 7 ⊢ (i‘1) = (〈0R, 1R〉‘1) |
22 | df-fv 6366 | . . . . . . 7 ⊢ (〈0R, 1R〉‘1) = (℩𝑦1〈0R, 1R〉𝑦) | |
23 | 21, 22 | eqtri 2759 | . . . . . 6 ⊢ (i‘1) = (℩𝑦1〈0R, 1R〉𝑦) |
24 | 23 | breq2i 5047 | . . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦)) |
25 | df-r 10704 | . . . . . . 7 ⊢ ℝ = (R × {0R}) | |
26 | sseq2 3913 | . . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R}))) | |
27 | 26 | abbidv 2800 | . . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}) |
28 | df-pw 4501 | . . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ} | |
29 | df-pw 4501 | . . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})} | |
30 | 27, 28, 29 | 3eqtr4g 2796 | . . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R})) |
31 | 25, 30 | ax-mp 5 | . . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R}) |
32 | 31 | breqi 5045 | . . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦)) |
33 | 24, 32 | bitri 278 | . . . 4 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦)) |
34 | 33 | anbi1i 627 | . . 3 ⊢ ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1))) |
35 | 34 | notbii 323 | . 2 ⊢ (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1))) |
36 | 19, 35 | mpbir 234 | 1 ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 399 = wceq 1543 ∈ wcel 2112 {cab 2714 Vcvv 3398 ⊆ wss 3853 ∅c0 4223 𝒫 cpw 4499 {csn 4527 〈cop 4533 class class class wbr 5039 × cxp 5534 ℩cio 6314 ‘cfv 6358 (class class class)co 7191 Rcnr 10444 0Rc0r 10445 1Rc1r 10446 ℝcr 10693 0cc0 10694 1c1 10695 ici 10696 · cmul 10699 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-12 2177 ax-ext 2708 ax-resscn 10751 ax-1cn 10752 ax-icn 10753 ax-addcl 10754 ax-mulcl 10756 ax-mulcom 10758 ax-mulass 10760 ax-distr 10761 ax-i2m1 10762 ax-1rid 10764 ax-cnre 10767 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-iota 6316 df-fv 6366 df-ov 7194 df-i 10703 df-r 10704 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |