Description: Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of TakeutiZaring p. 38. (Contributed by NM, 18-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ordsson | |- ( Ord A -> A C_ On ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ordon | |- Ord On |
|
| 2 | ordeleqon | |- ( Ord A <-> ( A e. On \/ A = On ) ) |
|
| 3 | 2 | birani | |- ( ( Ord A /\ Ord On ) -> ( A e. On \/ A = On ) ) |
| 4 | ordsseleq | |- ( ( Ord A /\ Ord On ) -> ( A C_ On <-> ( A e. On \/ A = On ) ) ) |
|
| 5 | 3 4 | mpbird | |- ( ( Ord A /\ Ord On ) -> A C_ On ) |
| 6 | 1 5 | mpan2 | |- ( Ord A -> A C_ On ) |