![]() |
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 2015 | . . . . . . . 8 ⊢ 𝑥 = 𝑥 | |
2 | dfnul2 4284 | . . . . . . . . . 10 ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | |
3 | 2 | abeq2i 2879 | . . . . . . . . 9 ⊢ (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥) |
4 | 3 | con2bii 357 | . . . . . . . 8 ⊢ (𝑥 = 𝑥 ↔ ¬ 𝑥 ∈ ∅) |
5 | 1, 4 | mpbi 229 | . . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅ |
6 | eleq1 2825 | . . . . . . 7 ⊢ (𝑥 = 〈𝐹, 0〉 → (𝑥 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅)) | |
7 | 5, 6 | mtbii 325 | . . . . . 6 ⊢ (𝑥 = 〈𝐹, 0〉 → ¬ 〈𝐹, 0〉 ∈ ∅) |
8 | 7 | vtocleg 3513 | . . . . 5 ⊢ (〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
9 | elex 3462 | . . . . . 6 ⊢ (〈𝐹, 0〉 ∈ ∅ → 〈𝐹, 0〉 ∈ V) | |
10 | 9 | con3i 154 | . . . . 5 ⊢ (¬ 〈𝐹, 0〉 ∈ V → ¬ 〈𝐹, 0〉 ∈ ∅) |
11 | 8, 10 | pm2.61i 182 | . . . 4 ⊢ ¬ 〈𝐹, 0〉 ∈ ∅ |
12 | df-br 5105 | . . . . 5 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, (0 · 1)〉 ∈ ∅) | |
13 | 0cn 11144 | . . . . . . . 8 ⊢ 0 ∈ ℂ | |
14 | 13 | mulid1i 11156 | . . . . . . 7 ⊢ (0 · 1) = 0 |
15 | 14 | opeq2i 4833 | . . . . . 6 ⊢ 〈𝐹, (0 · 1)〉 = 〈𝐹, 0〉 |
16 | 15 | eleq1i 2828 | . . . . 5 ⊢ (〈𝐹, (0 · 1)〉 ∈ ∅ ↔ 〈𝐹, 0〉 ∈ ∅) |
17 | 12, 16 | bitri 274 | . . . 4 ⊢ (𝐹∅(0 · 1) ↔ 〈𝐹, 0〉 ∈ ∅) |
18 | 11, 17 | mtbir 322 | . . 3 ⊢ ¬ 𝐹∅(0 · 1) |
19 | 18 | intnan 487 | . 2 ⊢ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1)) |
20 | df-i 11057 | . . . . . . . 8 ⊢ i = 〈0R, 1R〉 | |
21 | 20 | fveq1i 6841 | . . . . . . 7 ⊢ (i‘1) = (〈0R, 1R〉‘1) |
22 | df-fv 6502 | . . . . . . 7 ⊢ (〈0R, 1R〉‘1) = (℩𝑦1〈0R, 1R〉𝑦) | |
23 | 21, 22 | eqtri 2764 | . . . . . 6 ⊢ (i‘1) = (℩𝑦1〈0R, 1R〉𝑦) |
24 | 23 | breq2i 5112 | . . . . 5 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦)) |
25 | df-r 11058 | . . . . . . 7 ⊢ ℝ = (R × {0R}) | |
26 | sseq2 3969 | . . . . . . . . 9 ⊢ (ℝ = (R × {0R}) → (𝑧 ⊆ ℝ ↔ 𝑧 ⊆ (R × {0R}))) | |
27 | 26 | abbidv 2805 | . . . . . . . 8 ⊢ (ℝ = (R × {0R}) → {𝑧 ∣ 𝑧 ⊆ ℝ} = {𝑧 ∣ 𝑧 ⊆ (R × {0R})}) |
28 | df-pw 4561 | . . . . . . . 8 ⊢ 𝒫 ℝ = {𝑧 ∣ 𝑧 ⊆ ℝ} | |
29 | df-pw 4561 | . . . . . . . 8 ⊢ 𝒫 (R × {0R}) = {𝑧 ∣ 𝑧 ⊆ (R × {0R})} | |
30 | 27, 28, 29 | 3eqtr4g 2801 | . . . . . . 7 ⊢ (ℝ = (R × {0R}) → 𝒫 ℝ = 𝒫 (R × {0R})) |
31 | 25, 30 | ax-mp 5 | . . . . . 6 ⊢ 𝒫 ℝ = 𝒫 (R × {0R}) |
32 | 31 | breqi 5110 | . . . . 5 ⊢ (𝐴𝒫 ℝ(℩𝑦1〈0R, 1R〉𝑦) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦)) |
33 | 24, 32 | bitri 274 | . . . 4 ⊢ (𝐴𝒫 ℝ(i‘1) ↔ 𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦)) |
34 | 33 | anbi1i 624 | . . 3 ⊢ ((𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1))) |
35 | 34 | notbii 319 | . 2 ⊢ (¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) ↔ ¬ (𝐴𝒫 (R × {0R})(℩𝑦1〈0R, 1R〉𝑦) ∧ 𝐹∅(0 · 1))) |
36 | 19, 35 | mpbir 230 | 1 ⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {cab 2713 Vcvv 3444 ⊆ wss 3909 ∅c0 4281 𝒫 cpw 4559 {csn 4585 〈cop 4591 class class class wbr 5104 × cxp 5630 ℩cio 6444 ‘cfv 6494 (class class class)co 7354 Rcnr 10798 0Rc0r 10799 1Rc1r 10800 ℝcr 11047 0cc0 11048 1c1 11049 ici 11050 · cmul 11053 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-12 2171 ax-ext 2707 ax-resscn 11105 ax-1cn 11106 ax-icn 11107 ax-addcl 11108 ax-mulcl 11110 ax-mulcom 11112 ax-mulass 11114 ax-distr 11115 ax-i2m1 11116 ax-1rid 11118 ax-cnre 11121 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-iota 6446 df-fv 6502 df-ov 7357 df-i 11057 df-r 11058 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |