Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  avril1 Structured version   Unicode version

Theorem avril1 25588
 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 http://us.metamath.org/mpeuni/mmnotes.txt, under the 1-Apr-2006 entry.
Assertion
Ref Expression
avril1

Proof of Theorem avril1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 equid 1815 . . . . . . . 8
2 dfnul2 3740 . . . . . . . . . 10
32abeq2i 2529 . . . . . . . . 9
43con2bii 330 . . . . . . . 8
51, 4mpbi 208 . . . . . . 7
6 eleq1 2474 . . . . . . 7
75, 6mtbii 300 . . . . . 6
87vtocleg 3130 . . . . 5
9 elex 3068 . . . . . 6
109con3i 135 . . . . 5
118, 10pm2.61i 164 . . . 4
12 df-br 4396 . . . . 5
13 0cn 9618 . . . . . . . 8
1413mulid1i 9628 . . . . . . 7
1514opeq2i 4163 . . . . . 6
1615eleq1i 2479 . . . . 5
1712, 16bitri 249 . . . 4
1811, 17mtbir 297 . . 3
1918intnan 915 . 2
20 df-i 9531 . . . . . . . 8
2120fveq1i 5850 . . . . . . 7
22 df-fv 5577 . . . . . . 7
2321, 22eqtri 2431 . . . . . 6
2423breq2i 4403 . . . . 5
25 df-r 9532 . . . . . . 7
26 sseq2 3464 . . . . . . . . 9
2726abbidv 2538 . . . . . . . 8
28 df-pw 3957 . . . . . . . 8
29 df-pw 3957 . . . . . . . 8
3027, 28, 293eqtr4g 2468 . . . . . . 7
3125, 30ax-mp 5 . . . . . 6
3231breqi 4401 . . . . 5
3324, 32bitri 249 . . . 4
3433anbi1i 693 . . 3
3534notbii 294 . 2
3619, 35mpbir 209 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wa 367   wceq 1405   wcel 1842  cab 2387  cvv 3059   wss 3414  c0 3738  cpw 3955  csn 3972  cop 3978   class class class wbr 4395   cxp 4821  cio 5531  cfv 5569  (class class class)co 6278  cnr 9273  c0r 9274  c1r 9275  cr 9521  cc0 9522  c1 9523  ci 9524   cmul 9527 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-mulcl 9584  ax-mulcom 9586  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1rid 9592  ax-cnre 9595 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-iota 5533  df-fv 5577  df-ov 6281  df-i 9531  df-r 9532 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator