| 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 1159 |
. . . . . . . 8
| |
| 2 | dfnul2 2332 |
. . . . . . . . . 10
| |
| 3 | 2 | abeq2i 1611 |
. . . . . . . . 9
|
| 4 | 3 | con2bii 219 |
. . . . . . . 8
|
| 5 | 1, 4 | mpbi 187 |
. . . . . . 7
|
| 6 | eleq1 1575 |
. . . . . . 7
| |
| 7 | 5, 6 | mtbii 719 |
. . . . . 6
|
| 8 | 7 | vtocleg 1899 |
. . . . 5
|
| 9 | elisset 1861 |
. . . . . 6
| |
| 10 | 9 | con3i 98 |
. . . . 5
|
| 11 | 8, 10 | pm2.61i 124 |
. . . 4
|
| 12 | df-br 2688 |
. . . . 5
| |
| 13 | 0cn 5473 |
. . . . . . . 8
| |
| 14 | 13 | mulid1i 5477 |
. . . . . . 7
|
| 15 | 14 | opeq2i 2551 |
. . . . . 6
|
| 16 | 15 | eleq1i 1578 |
. . . . 5
|
| 17 | 12, 16 | bitri 171 |
. . . 4
|
| 18 | 11, 17 | mtbir 190 |
. . 3
|
| 19 | 18 | intnan 694 |
. 2
|
| 20 | df-i 5388 |
. . . . . . . 8
| |
| 21 | 20 | fveq1i 3832 |
. . . . . . 7
|
| 22 | df-fv 3276 |
. . . . . . 7
| |
| 23 | 21, 22 | eqtri 1536 |
. . . . . 6
|
| 24 | 23 | breq2i 2695 |
. . . . 5
|
| 25 | df-r 5389 |
. . . . . . 7
| |
| 26 | sseq2 2133 |
. . . . . . . . 9
| |
| 27 | 26 | abbidv 1618 |
. . . . . . . 8
|
| 28 | df-pw 2454 |
. . . . . . . 8
| |
| 29 | df-pw 2454 |
. . . . . . . 8
| |
| 30 | 27, 28, 29 | 3eqtr4g 1572 |
. . . . . . 7
|
| 31 | 25, 30 | ax-mp 7 |
. . . . . 6
|
| 32 | 31 | breqi 2693 |
. . . . 5
|
| 33 | 24, 32 | bitri 171 |
. . . 4
|
| 34 | 33 | anbi1i 483 |
. . 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 995 ax-gen 996 ax-8 997 ax-9 998 ax-10 999 ax-11 1000 ax-12 1001 ax-13 1002 ax-14 1003 ax-17 1004 ax-4 1006 ax-5o 1008 ax-6o 1011 ax-9o 1156 ax-10o 1174 ax-16 1244 ax-11o 1252 ax-ext 1498 ax-rep 2763 ax-sep 2773 ax-nul 2780 ax-pow 2813 ax-pr 2851 ax-un 3086 ax-inf2 4761 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 779 df-3an 780 df-ex 1014 df-sb 1206 df-eu 1419 df-mo 1420 df-clab 1504 df-cleq 1509 df-clel 1512 df-ne 1628 df-ral 1693 df-rex 1694 df-reu 1695 df-rab 1696 df-v 1856 df-sbc 1985 df-csb 2050 df-dif 2099 df-un 2100 df-in 2101 df-ss 2103 df-pss 2105 df-nul 2331 df-if 2414 df-pw 2454 df-sn 2465 df-pr 2466 df-tp 2468 df-op 2469 df-uni 2565 df-int 2596 df-iun 2630 df-br 2688 df-opab 2736 df-tr 2750 df-eprel 2906 df-id 2909 df-po 2914 df-so 2926 df-fr 2944 df-we 2959 df-ord 2975 df-on 2976 df-lim 2977 df-suc 2978 df-om 3216 df-xp 3262 df-rel 3263 df-cnv 3264 df-co 3265 df-dm 3266 df-rn 3267 df-res 3268 df-ima 3269 df-fun 3270 df-fn 3271 df-f 3272 df-fv 3276 df-opr 4018 df-oprab 4019 df-1st 4135 df-2nd 4136 df-rdg 4228 df-1o 4264 df-oadd 4266 df-omul 4267 df-er 4396 df-ec 4398 df-qs 4401 df-ni 5145 df-pli 5146 df-mi 5147 df-lti 5148 df-plpq 5180 df-mpq 5181 df-enq 5182 df-nq 5183 df-plq 5184 df-mq 5185 df-rq 5186 df-ltq 5187 df-1q 5188 df-np 5231 df-1p 5232 df-plp 5233 df-mp 5234 df-ltp 5235 df-plpr 5309 df-mpr 5310 df-enr 5311 df-nr 5312 df-plr 5313 df-mr 5314 df-0r 5316 df-1r 5317 df-m1r 5318 df-c 5385 df-0 5386 df-1 5387 df-i 5388 df-r 5389 df-plus 5390 df-mul 5391 |