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

Theorem avril1 29706
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.

Assertion
Ref Expression
avril1 ยฌ (๐ด๐’ซ โ„(iโ€˜1) โˆง ๐นโˆ…(0 ยท 1))

Proof of Theorem avril1
Dummy variable ๐‘ฅ is distinct from all other variables.
StepHypRef Expression
1 equid 2016 . . . . . . . 8 ๐‘ฅ = ๐‘ฅ
2 dfnul2 4325 . . . . . . . . . 10 โˆ… = {๐‘ฅ โˆฃ ยฌ ๐‘ฅ = ๐‘ฅ}
32eqabri 2878 . . . . . . . . 9 (๐‘ฅ โˆˆ โˆ… โ†” ยฌ ๐‘ฅ = ๐‘ฅ)
43con2bii 358 . . . . . . . 8 (๐‘ฅ = ๐‘ฅ โ†” ยฌ ๐‘ฅ โˆˆ โˆ…)
51, 4mpbi 229 . . . . . . 7 ยฌ ๐‘ฅ โˆˆ โˆ…
6 eleq1 2822 . . . . . . 7 (๐‘ฅ = โŸจ๐น, 0โŸฉ โ†’ (๐‘ฅ โˆˆ โˆ… โ†” โŸจ๐น, 0โŸฉ โˆˆ โˆ…))
75, 6mtbii 326 . . . . . 6 (๐‘ฅ = โŸจ๐น, 0โŸฉ โ†’ ยฌ โŸจ๐น, 0โŸฉ โˆˆ โˆ…)
87vtocleg 3546 . . . . 5 (โŸจ๐น, 0โŸฉ โˆˆ V โ†’ ยฌ โŸจ๐น, 0โŸฉ โˆˆ โˆ…)
9 elex 3493 . . . . . 6 (โŸจ๐น, 0โŸฉ โˆˆ โˆ… โ†’ โŸจ๐น, 0โŸฉ โˆˆ V)
109con3i 154 . . . . 5 (ยฌ โŸจ๐น, 0โŸฉ โˆˆ V โ†’ ยฌ โŸจ๐น, 0โŸฉ โˆˆ โˆ…)
118, 10pm2.61i 182 . . . 4 ยฌ โŸจ๐น, 0โŸฉ โˆˆ โˆ…
12 df-br 5149 . . . . 5 (๐นโˆ…(0 ยท 1) โ†” โŸจ๐น, (0 ยท 1)โŸฉ โˆˆ โˆ…)
13 0cn 11203 . . . . . . . 8 0 โˆˆ โ„‚
1413mulridi 11215 . . . . . . 7 (0 ยท 1) = 0
1514opeq2i 4877 . . . . . 6 โŸจ๐น, (0 ยท 1)โŸฉ = โŸจ๐น, 0โŸฉ
1615eleq1i 2825 . . . . 5 (โŸจ๐น, (0 ยท 1)โŸฉ โˆˆ โˆ… โ†” โŸจ๐น, 0โŸฉ โˆˆ โˆ…)
1712, 16bitri 275 . . . 4 (๐นโˆ…(0 ยท 1) โ†” โŸจ๐น, 0โŸฉ โˆˆ โˆ…)
1811, 17mtbir 323 . . 3 ยฌ ๐นโˆ…(0 ยท 1)
1918intnan 488 . 2 ยฌ (๐ด๐’ซ (R ร— {0R})(โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ) โˆง ๐นโˆ…(0 ยท 1))
20 df-i 11116 . . . . . . . 8 i = โŸจ0R, 1RโŸฉ
2120fveq1i 6890 . . . . . . 7 (iโ€˜1) = (โŸจ0R, 1RโŸฉโ€˜1)
22 df-fv 6549 . . . . . . 7 (โŸจ0R, 1RโŸฉโ€˜1) = (โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ)
2321, 22eqtri 2761 . . . . . 6 (iโ€˜1) = (โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ)
2423breq2i 5156 . . . . 5 (๐ด๐’ซ โ„(iโ€˜1) โ†” ๐ด๐’ซ โ„(โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ))
25 df-r 11117 . . . . . . 7 โ„ = (R ร— {0R})
26 sseq2 4008 . . . . . . . . 9 (โ„ = (R ร— {0R}) โ†’ (๐‘ง โŠ† โ„ โ†” ๐‘ง โŠ† (R ร— {0R})))
2726abbidv 2802 . . . . . . . 8 (โ„ = (R ร— {0R}) โ†’ {๐‘ง โˆฃ ๐‘ง โŠ† โ„} = {๐‘ง โˆฃ ๐‘ง โŠ† (R ร— {0R})})
28 df-pw 4604 . . . . . . . 8 ๐’ซ โ„ = {๐‘ง โˆฃ ๐‘ง โŠ† โ„}
29 df-pw 4604 . . . . . . . 8 ๐’ซ (R ร— {0R}) = {๐‘ง โˆฃ ๐‘ง โŠ† (R ร— {0R})}
3027, 28, 293eqtr4g 2798 . . . . . . 7 (โ„ = (R ร— {0R}) โ†’ ๐’ซ โ„ = ๐’ซ (R ร— {0R}))
3125, 30ax-mp 5 . . . . . 6 ๐’ซ โ„ = ๐’ซ (R ร— {0R})
3231breqi 5154 . . . . 5 (๐ด๐’ซ โ„(โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ) โ†” ๐ด๐’ซ (R ร— {0R})(โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ))
3324, 32bitri 275 . . . 4 (๐ด๐’ซ โ„(iโ€˜1) โ†” ๐ด๐’ซ (R ร— {0R})(โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ))
3433anbi1i 625 . . 3 ((๐ด๐’ซ โ„(iโ€˜1) โˆง ๐นโˆ…(0 ยท 1)) โ†” (๐ด๐’ซ (R ร— {0R})(โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ) โˆง ๐นโˆ…(0 ยท 1)))
3534notbii 320 . 2 (ยฌ (๐ด๐’ซ โ„(iโ€˜1) โˆง ๐นโˆ…(0 ยท 1)) โ†” ยฌ (๐ด๐’ซ (R ร— {0R})(โ„ฉ๐‘ฆ1โŸจ0R, 1RโŸฉ๐‘ฆ) โˆง ๐นโˆ…(0 ยท 1)))
3619, 35mpbir 230 1 ยฌ (๐ด๐’ซ โ„(iโ€˜1) โˆง ๐นโˆ…(0 ยท 1))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107  {cab 2710  Vcvv 3475   โŠ† wss 3948  โˆ…c0 4322  ๐’ซ cpw 4602  {csn 4628  โŸจcop 4634   class class class wbr 5148   ร— cxp 5674  โ„ฉcio 6491  โ€˜cfv 6541  (class class class)co 7406  Rcnr 10857  0Rc0r 10858  1Rc1r 10859  โ„cr 11106  0cc0 11107  1c1 11108  ici 11109   ยท cmul 11112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-mulcl 11169  ax-mulcom 11171  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1rid 11177  ax-cnre 11180
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409  df-i 11116  df-r 11117
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator