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 A Ord A

Proof

Step Hyp Ref Expression
1 ordsson Ord A A On
2 ssorduni A On Ord A
3 1 2 syl Ord A Ord A