| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode 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
germanus
dictum sit, altum viditur, often used in set theory. Starting with
the
seemingly simple yet profound fact that any object A reply to skeptics can be found at http://us.metamath.org/mpegif/mmnotes.txt, under the 1-Apr-2006 entry. |
| Ref | Expression |
|---|---|
| avril1 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equid 1162 |
. . . . . . . 8
| |
| 2 | dfnul2 2334 |
. . . . . . . . . 10
| |
| 3 | 2 | abeq2i 1613 |
. . . . . . . . 9
|
| 4 | 3 | con2bii 219 |
. . . . . . . 8
|
| 5 | 1, 4 | mpbi 187 |
. . . . . . 7
|
| 6 | eleq1 1577 |
. . . . . . 7
| |
| 7 | 5, 6 | mtbii 721 |
. . . . . 6
|
| 8 | 7 | vtocleg 1901 |
. . . . 5
|
| 9 | elisset 1863 |
. . . . . 6
| |
| 10 | 9 | con3i 98 |
. . . . 5
|
| 11 | 8, 10 | pm2.61i 124 |
. . . 4
|
| 12 | df-br 2693 |
. . . . 5
| |
| 13 | 0cn 5482 |
. . . . . . . 8
| |
| 14 | 13 | mulid1i 5486 |
. . . . . . 7
|
| 15 | 14 | opeq2i 2556 |
. . . . . 6
|
| 16 | 15 | eleq1i 1580 |
. . . . 5
|
| 17 | 12, 16 | bitri 171 |
. . . 4
|
| 18 | 11, 17 | mtbir 190 |
. . 3
|
| 19 | 18 | intnan 695 |
. 2
|
| 20 | df-i 5397 |
. . . . . . . 8
| |
| 21 | 20 | fveq1i 3836 |
. . . . . . 7
|
| 22 | df-fv 3279 |
. . . . . . 7
| |
| 23 | 21, 22 | eqtri 1538 |
. . . . . 6
|
| 24 | 23 | breq2i 2700 |
. . . . 5
|
| 25 | df-r 5398 |
. . . . . . 7
| |
| 26 | sseq2 2135 |
. . . . . . . . 9
| |
| 27 | 26 | abbidv 1620 |
. . . . . . . 8
|
| 28 | df-pw 2459 |
. . . . . . . 8
| |
| 29 | df-pw 2459 |
. . . . . . . 8
| |
| 30 | 27, 28, 29 | 3eqtr4g 1574 |
. . . . . . 7
|
| 31 | 25, 30 | ax-mp 7 |
. . . . . 6
|
| 32 | 31 | breqi 2698 |
. . . . 5
|
| 33 | 24, 32 | bitri 171 |
. . . 4
|
| 34 | 33 | anbi1i 484 |
. . 3
|
| 35 | 34 | notbii 185 |
. 2
|
| 36 | 19, 35 | mpbir 188 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089 ax-inf2 4770 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-ral 1695 df-rex 1696 df-reu 1697 df-rab 1698 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-pss 2107 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-int 2601 df-iun 2635 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-fv 3279 df-opr 4023 df-oprab 4024 df-1st 4140 df-2nd 4141 df-rdg 4233 df-1o 4269 df-oadd 4271 df-omul 4272 df-er 4401 df-ec 4403 df-qs 4406 df-ni 5154 df-pli 5155 df-mi 5156 df-lti 5157 df-plpq 5189 df-mpq 5190 df-enq 5191 df-nq 5192 df-plq 5193 df-mq 5194 df-rq 5195 df-ltq 5196 df-1q 5197 df-np 5240 df-1p 5241 df-plp 5242 df-mp 5243 df-ltp 5244 df-plpr 5318 df-mpr 5319 df-enr 5320 df-nr 5321 df-plr 5322 df-mr 5323 df-0r 5325 df-1r 5326 df-m1r 5327 df-c 5394 df-0 5395 df-1 5396 df-i 5397 df-r 5398 df-plus 5399 df-mul 5400 |