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 | biimpi | |- ( Ord A -> ( A e. On \/ A = On ) ) |
| 4 | 3 | adantr | |- ( ( Ord A /\ Ord On ) -> ( A e. On \/ A = On ) ) |
| 5 | ordsseleq | |- ( ( Ord A /\ Ord On ) -> ( A C_ On <-> ( A e. On \/ A = On ) ) ) |
|
| 6 | 4 5 | mpbird | |- ( ( Ord A /\ Ord On ) -> A C_ On ) |
| 7 | 1 6 | mpan2 | |- ( Ord A -> A C_ On ) |