![]() |
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 2096 | . . . . . . . 8 ⊢ 𝑥 = 𝑥 | |
2 | dfnul2 4063 | . . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | |
3 | 2 | abeq2i 2883 | . . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥) |
4 | 3 | con2bii 346 | . . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅) |
5 | 1, 4 | mpbi 220 | . . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅ |
6 | eleq1 2837 | . . . . . . 7 ⊢ (𝑥 = 〈𝐹, 0〉 → (𝑥 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅)) | |
7 | 5, 6 | mtbii 315 | . . . . . 6 ⊢ (𝑥 = 〈𝐹, 0〉 → ¬ 〈𝐹, 0〉 ∈ ∅) |
8 | 7 | vtocleg 3428 | . . . . 5 ⊢ (〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
9 | elex 3361 | . . . . . 6 ⊢ (〈𝐹, 0〉 ∈ ∅ → 〈𝐹, 0〉 ∈ V) | |
10 | 9 | con3i 151 | . . . . 5 ⊢ (¬ 〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
11 | 8, 10 | pm2.61i 176 | . . . 4 ⊢ ¬ 〈𝐹, 0〉 ∈ ∅ |
12 | df-br 4785 | . . . . 5 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, (0 · 1)〉 ∈ ∅) | |
13 | 0cn 10233 | . . . . . . . 8 ⊢ 0 ∈ ℂ | |
14 | 13 | mulid1i 10243 | . . . . . . 7 ⊢ (0 · 1) = 0 |
15 | 14 | opeq2i 4541 | . . . . . 6 ⊢ 〈𝐹, (0 · 1)〉 = 〈𝐹, 0〉 |
16 | 15 | eleq1i 2840 | . . . . 5 ⊢ (〈𝐹, (0 · 1)〉 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅) |
17 | 12, 16 | bitri 264 | . . . 4 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, 0〉 ∈ ∅) |
18 | 11, 17 | mtbir 312 | . . 3 ⊢ ¬ 𝐹∅(0 · 1) |
19 | 18 | intnan 996 | . 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1)) |
20 | df-i 10146 | . . . . . . . 8 ⊢ i = 〈0R, 1R〉 | |
21 | 20 | fveq1i 6333 | . . . . . . 7 ⊢ (i‘1) = (〈0R, 1R〉‘1) |
22 | df-fv 6039 | . . . . . . 7 ⊢ (〈0R, 1R〉‘1) = (℩𝑦1〈0R, 1R〉𝑦) | |
23 | 21, 22 | eqtri 2792 | . . . . . 6 ⊢ (i‘1) = (℩𝑦1〈0R, 1R〉𝑦) |
24 | 23 | breq2i 4792 | . . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦)) |
25 | df-r 10147 | . . . . . . 7 ⊢ ℝ = (R × {0R}) | |
26 | sseq2 3774 | . . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R}))) | |
27 | 26 | abbidv 2889 | . . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}) |
28 | df-pw 4297 | . . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ} | |
29 | df-pw 4297 | . . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})} | |
30 | 27, 28, 29 | 3eqtr4g 2829 | . . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R})) |
31 | 25, 30 | ax-mp 5 | . . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R}) |
32 | 31 | breqi 4790 | . . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦)) |
33 | 24, 32 | bitri 264 | . . . 4 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦)) |
34 | 33 | anbi1i 602 | . . 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 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 |