# Metamath Proof Explorer

## Theorem ordsson

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 ${⊢}\mathrm{Ord}{A}\to {A}\subseteq \mathrm{On}$

### Proof

Step Hyp Ref Expression
1 ordon ${⊢}\mathrm{Ord}\mathrm{On}$
2 ordeleqon ${⊢}\mathrm{Ord}{A}↔\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)$
3 2 biimpi ${⊢}\mathrm{Ord}{A}\to \left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)$
4 3 adantr ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}\mathrm{On}\right)\to \left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)$
5 ordsseleq ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}\mathrm{On}\right)\to \left({A}\subseteq \mathrm{On}↔\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)\right)$
6 4 5 mpbird ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}\mathrm{On}\right)\to {A}\subseteq \mathrm{On}$
7 1 6 mpan2 ${⊢}\mathrm{Ord}{A}\to {A}\subseteq \mathrm{On}$