Metamath Proof Explorer


Theorem orduni

Description: The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003)

Ref Expression
Assertion orduni ( Ord 𝐴 → Ord 𝐴 )

Proof

Step Hyp Ref Expression
1 ordsson ( Ord 𝐴𝐴 ⊆ On )
2 ssorduni ( 𝐴 ⊆ On → Ord 𝐴 )
3 1 2 syl ( Ord 𝐴 → Ord 𝐴 )