This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trssord

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

Ref Expression
Assertion trssord ⊢ Tr ⁡ A ∧ A ⊆ B ∧ Ord ⁡ B → Ord ⁡ A

Proof

Step Hyp Ref Expression
1 wess ⊢ A ⊆ B → E We B → E We A
2 ordwe ⊢ Ord ⁡ B → E We B
3 1 2 impel ⊢ A ⊆ B ∧ Ord ⁡ B → E We A
4 3 anim2i ⊢ Tr ⁡ A ∧ A ⊆ B ∧ Ord ⁡ B → Tr ⁡ A ∧ E We A
5 4 3impb ⊢ Tr ⁡ A ∧ A ⊆ B ∧ Ord ⁡ B → Tr ⁡ A ∧ E We A
6 df-ord ⊢ Ord ⁡ A ↔ Tr ⁡ A ∧ E We A
7 5 6 sylibr ⊢ Tr ⁡ A ∧ A ⊆ B ∧ Ord ⁡ B → Ord ⁡ A