Metamath Proof Explorer


Theorem ssonuni

Description: The union of a set of ordinal numbers is an ordinal number. Theorem 9 of Suppes p. 132. Lemma 2.7 of Schloeder p. 4. (Contributed by NM, 1-Nov-2003)

Ref Expression
Assertion ssonuni A V A On A On

Proof

Step Hyp Ref Expression
1 ssorduni A On Ord A
2 uniexg A V A V
3 elong A V A On Ord A
4 2 3 syl A V A On Ord A
5 1 4 imbitrrid A V A On A On