![]() |
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 1985 | . . . . . . . 8 ⊢ 𝑥 = 𝑥 | |
2 | dfnul2 3950 | . . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | |
3 | 2 | abeq2i 2764 | . . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥) |
4 | 3 | con2bii 346 | . . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅) |
5 | 1, 4 | mpbi 220 | . . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅ |
6 | eleq1 2718 | . . . . . . 7 ⊢ (𝑥 = 〈𝐹, 0〉 → (𝑥 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅)) | |
7 | 5, 6 | mtbii 315 | . . . . . 6 ⊢ (𝑥 = 〈𝐹, 0〉 → ¬ 〈𝐹, 0〉 ∈ ∅) |
8 | 7 | vtocleg 3310 | . . . . 5 ⊢ (〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
9 | elex 3243 | . . . . . 6 ⊢ (〈𝐹, 0〉 ∈ ∅ → 〈𝐹, 0〉 ∈ V) | |
10 | 9 | con3i 150 | . . . . 5 ⊢ (¬ 〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
11 | 8, 10 | pm2.61i 176 | . . . 4 ⊢ ¬ 〈𝐹, 0〉 ∈ ∅ |
12 | df-br 4686 | . . . . 5 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, (0 · 1)〉 ∈ ∅) | |
13 | 0cn 10070 | . . . . . . . 8 ⊢ 0 ∈ ℂ | |
14 | 13 | mulid1i 10080 | . . . . . . 7 ⊢ (0 · 1) = 0 |
15 | 14 | opeq2i 4437 | . . . . . 6 ⊢ 〈𝐹, (0 · 1)〉 = 〈𝐹, 0〉 |
16 | 15 | eleq1i 2721 | . . . . 5 ⊢ (〈𝐹, (0 · 1)〉 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅) |
17 | 12, 16 | bitri 264 | . . . 4 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, 0〉 ∈ ∅) |
18 | 11, 17 | mtbir 312 | . . 3 ⊢ ¬ 𝐹∅(0 · 1) |
19 | 18 | intnan 980 | . 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1)) |
20 | df-i 9983 | . . . . . . . 8 ⊢ i = 〈0R, 1R〉 | |
21 | 20 | fveq1i 6230 | . . . . . . 7 ⊢ (i‘1) = (〈0R, 1R〉‘1) |
22 | df-fv 5934 | . . . . . . 7 ⊢ (〈0R, 1R〉‘1) = (℩𝑦1〈0R, 1R〉𝑦) | |
23 | 21, 22 | eqtri 2673 | . . . . . 6 ⊢ (i‘1) = (℩𝑦1〈0R, 1R〉𝑦) |
24 | 23 | breq2i 4693 | . . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦)) |
25 | df-r 9984 | . . . . . . 7 ⊢ ℝ = (R × {0R}) | |
26 | sseq2 3660 | . . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R}))) | |
27 | 26 | abbidv 2770 | . . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}) |
28 | df-pw 4193 | . . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ} | |
29 | df-pw 4193 | . . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})} | |
30 | 27, 28, 29 | 3eqtr4g 2710 | . . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R})) |
31 | 25, 30 | ax-mp 5 | . . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R}) |
32 | 31 | breqi 4691 | . . . . 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 731 | . . 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 383 = wceq 1523 ∈ wcel 2030 {cab 2637 Vcvv 3231 ⊆ wss 3607 ∅c0 3948 𝒫 cpw 4191 {csn 4210 〈cop 4216 class class class wbr 4685 × cxp 5141 ℩cio 5887 ‘cfv 5926 (class class class)co 6690 Rcnr 9725 0Rc0r 9726 1Rc1r 9727 ℝcr 9973 0cc0 9974 1c1 9975 ici 9976 · cmul 9979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-mulcl 10036 ax-mulcom 10038 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1rid 10044 ax-cnre 10047 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-ov 6693 df-i 9983 df-r 9984 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |