| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. |
| Ref | Expression |
|---|---|
| onmindif |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ontri1 3695 |
. . . . . . . . . . 11
| |
| 2 | onsssuc 3757 |
. . . . . . . . . . 11
| |
| 3 | 1, 2 | bitr3d 589 |
. . . . . . . . . 10
|
| 4 | 3 | con1bid 586 |
. . . . . . . . 9
|
| 5 | ssel2 2616 |
. . . . . . . . 9
| |
| 6 | 4, 5 | sylan 497 |
. . . . . . . 8
|
| 7 | 6 | biimpd 170 |
. . . . . . 7
|
| 8 | 7 | exp31 407 |
. . . . . 6
|
| 9 | 8 | com23 36 |
. . . . 5
|
| 10 | 9 | imp4b 392 |
. . . 4
|
| 11 | eldif 2609 |
. . . 4
| |
| 12 | 10, 11 | syl5ib 223 |
. . 3
|
| 13 | 12 | r19.21aiv 2175 |
. 2
|
| 14 | elintg 3222 |
. . 3
| |
| 15 | 14 | adantl 424 |
. 2
|
| 16 | 13, 15 | mpbird 213 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: unblem3 5635 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-int 3215 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-suc 3663 |