| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) |
| Ref | Expression |
|---|---|
| ordom |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dftr2 3613 |
. . 3
| |
| 2 | ordelord 3865 |
. . . . . . . 8
| |
| 3 | 2 | expcom 495 |
. . . . . . 7
|
| 4 | limord 3901 |
. . . . . . . . . . . 12
| |
| 5 | ordtr 3857 |
. . . . . . . . . . . 12
| |
| 6 | trel 3618 |
. . . . . . . . . . . 12
| |
| 7 | 4, 5, 6 | 3syl 38 |
. . . . . . . . . . 11
|
| 8 | 7 | exp3a 496 |
. . . . . . . . . 10
|
| 9 | 8 | com12 26 |
. . . . . . . . 9
|
| 10 | 9 | a2d 19 |
. . . . . . . 8
|
| 11 | 10 | alimdv 1966 |
. . . . . . 7
|
| 12 | 3, 11 | anim12d 629 |
. . . . . 6
|
| 13 | visset 2572 |
. . . . . . 7
| |
| 14 | 13 | elom 4120 |
. . . . . 6
|
| 15 | visset 2572 |
. . . . . . 7
| |
| 16 | 15 | elom 4120 |
. . . . . 6
|
| 17 | 12, 14, 16 | 3imtr4g 333 |
. . . . 5
|
| 18 | 17 | imp 489 |
. . . 4
|
| 19 | 18 | ax-gen 1622 |
. . 3
|
| 20 | 1, 19 | mpgbir 1652 |
. 2
|
| 21 | omsson 4122 |
. 2
| |
| 22 | ordon 4040 |
. 2
| |
| 23 | trssord 3860 |
. 2
| |
| 24 | 20, 21, 22, 23 | mp3an 1494 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: elnn 4128 omon 4129 limom 4133 ssnlim 4136 peano5 4141 nnarcl 5490 oaabslem 5509 oaabs 5510 onomeneq 5848 ominf 5869 omsdomnn 5870 alephgeom 6229 omsublim 6243 iscard3 6283 cflim2 6350 omsublimOLD 16481 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1621 ax-gen 1622 ax-8 1623 ax-9 1624 ax-10 1625 ax-11 1626 ax-12 1627 ax-13 1628 ax-14 1629 ax-17 1634 ax-4 1637 ax-5o 1639 ax-6o 1642 ax-9o 1792 ax-10o 1810 ax-16 1883 ax-11o 1893 ax-ext 2152 ax-sep 3638 ax-nul 3645 ax-pow 3681 ax-pr 3719 ax-un 3961 |
| This theorem depends on definitions: df-bi 232 df-or 434 df-an 435 df-3or 1131 df-3an 1132 df-ex 1645 df-sb 1845 df-eu 2070 df-mo 2071 df-clab 2158 df-cleq 2163 df-clel 2166 df-ne 2297 df-ral 2389 df-rex 2390 df-rab 2392 df-v 2571 df-dif 2862 df-un 2864 df-in 2866 df-ss 2868 df-pss 2870 df-nul 3115 df-pw 3261 df-sn 3274 df-pr 3275 df-tp 3277 df-op 3278 df-uni 3399 df-br 3540 df-opab 3598 df-tr 3612 df-eprel 3776 df-po 3784 df-so 3796 df-fr 3814 df-we 3830 df-ord 3846 df-on 3847 df-lim 3848 df-suc 3849 df-om 4118 |