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 1926 | . . . . . . . 8 ⊢ 𝑥 = 𝑥 | |
2 | dfnul2 3876 | . . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | |
3 | 2 | abeq2i 2722 | . . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥) |
4 | 3 | con2bii 346 | . . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅) |
5 | 1, 4 | mpbi 219 | . . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅ |
6 | eleq1 2676 | . . . . . . 7 ⊢ (𝑥 = 〈𝐹, 0〉 → (𝑥 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅)) | |
7 | 5, 6 | mtbii 315 | . . . . . 6 ⊢ (𝑥 = 〈𝐹, 0〉 → ¬ 〈𝐹, 0〉 ∈ ∅) |
8 | 7 | vtocleg 3252 | . . . . 5 ⊢ (〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
9 | elex 3185 | . . . . . 6 ⊢ (〈𝐹, 0〉 ∈ ∅ → 〈𝐹, 0〉 ∈ V) | |
10 | 9 | con3i 149 | . . . . 5 ⊢ (¬ 〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
11 | 8, 10 | pm2.61i 175 | . . . 4 ⊢ ¬ 〈𝐹, 0〉 ∈ ∅ |
12 | df-br 4584 | . . . . 5 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, (0 · 1)〉 ∈ ∅) | |
13 | 0cn 9911 | . . . . . . . 8 ⊢ 0 ∈ ℂ | |
14 | 13 | mulid1i 9921 | . . . . . . 7 ⊢ (0 · 1) = 0 |
15 | 14 | opeq2i 4344 | . . . . . 6 ⊢ 〈𝐹, (0 · 1)〉 = 〈𝐹, 0〉 |
16 | 15 | eleq1i 2679 | . . . . 5 ⊢ (〈𝐹, (0 · 1)〉 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅) |
17 | 12, 16 | bitri 263 | . . . 4 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, 0〉 ∈ ∅) |
18 | 11, 17 | mtbir 312 | . . 3 ⊢ ¬ 𝐹∅(0 · 1) |
19 | 18 | intnan 951 | . 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1)) |
20 | df-i 9824 | . . . . . . . 8 ⊢ i = 〈0R, 1R〉 | |
21 | 20 | fveq1i 6104 | . . . . . . 7 ⊢ (i‘1) = (〈0R, 1R〉‘1) |
22 | df-fv 5812 | . . . . . . 7 ⊢ (〈0R, 1R〉‘1) = (℩𝑦1〈0R, 1R〉𝑦) | |
23 | 21, 22 | eqtri 2632 | . . . . . 6 ⊢ (i‘1) = (℩𝑦1〈0R, 1R〉𝑦) |
24 | 23 | breq2i 4591 | . . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦)) |
25 | df-r 9825 | . . . . . . 7 ⊢ ℝ = (R × {0R}) | |
26 | sseq2 3590 | . . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R}))) | |
27 | 26 | abbidv 2728 | . . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}) |
28 | df-pw 4110 | . . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ} | |
29 | df-pw 4110 | . . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})} | |
30 | 27, 28, 29 | 3eqtr4g 2669 | . . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R})) |
31 | 25, 30 | ax-mp 5 | . . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R}) |
32 | 31 | breqi 4589 | . . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦)) |
33 | 24, 32 | bitri 263 | . . . 4 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦)) |
34 | 33 | anbi1i 727 | . . 3 ⊢ ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1))) |
35 | 34 | notbii 309 | . 2 ⊢ (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1))) |
36 | 19, 35 | mpbir 220 | 1 ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 383 = wceq 1475 ∈ wcel 1977 {cab 2596 Vcvv 3173 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 〈cop 4131 class class class wbr 4583 × cxp 5036 ℩cio 5766 ‘cfv 5804 (class class class)co 6549 Rcnr 9566 0Rc0r 9567 1Rc1r 9568 ℝcr 9814 0cc0 9815 1c1 9816 ici 9817 · cmul 9820 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-mulcl 9877 ax-mulcom 9879 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1rid 9885 ax-cnre 9888 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 df-i 9824 df-r 9825 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |