Description: The class of finite ordinals _om is ordinal. Theorem 7.32 of TakeutiZaring p. 43. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ordom | |- Ord _om |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trom | |- Tr _om |
|
| 2 | omsson | |- _om C_ On |
|
| 3 | ordon | |- Ord On |
|
| 4 | trssord | |- ( ( Tr _om /\ _om C_ On /\ Ord On ) -> Ord _om ) |
|
| 5 | 1 2 3 4 | mp3an | |- Ord _om |