| 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 5479 |
. . . . . . . 8
| |
| 14 | 13 | mulid1i 5483 |
. . . . . . 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 5394 |
. . . . . . . 8
| |
| 21 | 20 | fveq1i 3834 |
. . . . . . 7
|
| 22 | df-fv 3278 |
. . . . . . 7
| |
| 23 | 21, 22 | eqtri 1536 |
. . . . . 6
|
| 24 | 23 | breq2i 2695 |
. . . . 5
|
| 25 | df-r 5395 |
. . . . . . 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 2814 ax-pr 2853 ax-un 3088 ax-inf2 4767 |
| 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 2908 df-id 2911 df-po 2916 df-so 2928 df-fr 2946 df-we 2961 df-ord 2977 df-on 2978 df-lim 2979 df-suc 2980 df-om 3218 df-xp 3264 df-rel 3265 df-cnv 3266 df-co 3267 df-dm 3268 df-rn 3269 df-res 3270 df-ima 3271 df-fun 3272 df-fn 3273 df-f 3274 df-fv 3278 df-opr 4020 df-oprab 4021 df-1st 4137 df-2nd 4138 df-rdg 4230 df-1o 4266 df-oadd 4268 df-omul 4269 df-er 4398 df-ec 4400 df-qs 4403 df-ni 5151 df-pli 5152 df-mi 5153 df-lti 5154 df-plpq 5186 df-mpq 5187 df-enq 5188 df-nq 5189 df-plq 5190 df-mq 5191 df-rq 5192 df-ltq 5193 df-1q 5194 df-np 5237 df-1p 5238 df-plp 5239 df-mp 5240 df-ltp 5241 df-plpr 5315 df-mpr 5316 df-enr 5317 df-nr 5318 df-plr 5319 df-mr 5320 df-0r 5322 df-1r 5323 df-m1r 5324 df-c 5391 df-0 5392 df-1 5393 df-i 5394 df-r 5395 df-plus 5396 df-mul 5397 |