| 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 1124 |
. . . . . . . 8
| |
| 2 | dfnul2 2278 |
. . . . . . . . . 10
| |
| 3 | 2 | abeq2i 1567 |
. . . . . . . . 9
|
| 4 | 3 | con2bii 221 |
. . . . . . . 8
|
| 5 | 1, 4 | mpbi 189 |
. . . . . . 7
|
| 6 | eleq1 1531 |
. . . . . . 7
| |
| 7 | 5, 6 | mtbii 715 |
. . . . . 6
|
| 8 | 7 | vtocleg 1851 |
. . . . 5
|
| 9 | elisset 1813 |
. . . . . 6
| |
| 10 | 9 | con3i 98 |
. . . . 5
|
| 11 | 8, 10 | pm2.61i 126 |
. . . 4
|
| 12 | df-br 2615 |
. . . . 5
| |
| 13 | 0cn 5308 |
. . . . . . . 8
| |
| 14 | 13 | mulid1 5312 |
. . . . . . 7
|
| 15 | 14 | opeq2i 2487 |
. . . . . 6
|
| 16 | 15 | eleq1i 1534 |
. . . . 5
|
| 17 | 12, 16 | bitr 173 |
. . . 4
|
| 18 | 11, 17 | mtbir 192 |
. . 3
|
| 19 | 18 | intnan 690 |
. 2
|
| 20 | df-i 5223 |
. . . . . . . 8
| |
| 21 | 20 | fveq1i 3716 |
. . . . . . 7
|
| 22 | df-fv 3193 |
. . . . . . 7
| |
| 23 | 21, 22 | eqtr 1492 |
. . . . . 6
|
| 24 | 23 | breq2i 2622 |
. . . . 5
|
| 25 | df-r 5224 |
. . . . . . 7
| |
| 26 | sseq2 2079 |
. . . . . . . . 9
| |
| 27 | 26 | abbidv 1574 |
. . . . . . . 8
|
| 28 | df-pw 2398 |
. . . . . . . 8
| |
| 29 | df-pw 2398 |
. . . . . . . 8
| |
| 30 | 27, 28, 29 | 3eqtr4g 1528 |
. . . . . . 7
|
| 31 | 25, 30 | ax-mp 7 |
. . . . . 6
|
| 32 | 31 | breqi 2620 |
. . . . 5
|
| 33 | 24, 32 | bitr 173 |
. . . 4
|
| 34 | 33 | anbi1i 481 |
. . 3
|
| 35 | 34 | negbii 187 |
. 2
|
| 36 | 19, 35 | mpbir 190 |
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 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-inf2 4605 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2499 df-int 2529 df-iun 2563 df-br 2615 df-opab 2662 df-tr 2676 df-eprel 2827 df-id 2830 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-on 2947 df-lim 2948 df-suc 2949 df-om 3127 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-fv 3193 df-rdg 3923 df-opr 3956 df-oprab 3957 df-1st 4069 df-2nd 4070 df-1o 4123 df-oadd 4125 df-omul 4126 df-er 4251 df-ec 4253 df-qs 4256 df-ni 4980 df-pli 4981 df-mi 4982 df-lti 4983 df-plpq 5015 df-mpq 5016 df-enq 5017 df-nq 5018 df-plq 5019 df-mq 5020 df-rq 5021 df-ltq 5022 df-1q 5023 df-np 5066 df-1p 5067 df-plp 5068 df-mp 5069 df-ltp 5070 df-plpr 5144 df-mpr 5145 df-enr 5146 df-nr 5147 df-plr 5148 df-mr 5149 df-0r 5151 df-1r 5152 df-m1r 5153 df-c 5220 df-0 5221 df-1 5222 df-i 5223 df-r 5224 df-plus 5225 df-mul 5226 |