# Metamath Proof Explorer

Description: A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994)

Ref Expression
Assertion trssord ${⊢}\left(\mathrm{Tr}{A}\wedge {A}\subseteq {B}\wedge \mathrm{Ord}{B}\right)\to \mathrm{Ord}{A}$

### Proof

Step Hyp Ref Expression
1 wess ${⊢}{A}\subseteq {B}\to \left(\mathrm{E}\mathrm{We}{B}\to \mathrm{E}\mathrm{We}{A}\right)$
2 ordwe ${⊢}\mathrm{Ord}{B}\to \mathrm{E}\mathrm{We}{B}$
3 1 2 impel ${⊢}\left({A}\subseteq {B}\wedge \mathrm{Ord}{B}\right)\to \mathrm{E}\mathrm{We}{A}$
4 3 anim2i ${⊢}\left(\mathrm{Tr}{A}\wedge \left({A}\subseteq {B}\wedge \mathrm{Ord}{B}\right)\right)\to \left(\mathrm{Tr}{A}\wedge \mathrm{E}\mathrm{We}{A}\right)$
5 4 3impb ${⊢}\left(\mathrm{Tr}{A}\wedge {A}\subseteq {B}\wedge \mathrm{Ord}{B}\right)\to \left(\mathrm{Tr}{A}\wedge \mathrm{E}\mathrm{We}{A}\right)$
6 df-ord ${⊢}\mathrm{Ord}{A}↔\left(\mathrm{Tr}{A}\wedge \mathrm{E}\mathrm{We}{A}\right)$
7 5 6 sylibr ${⊢}\left(\mathrm{Tr}{A}\wedge {A}\subseteq {B}\wedge \mathrm{Ord}{B}\right)\to \mathrm{Ord}{A}$