Metamath Proof Explorer


Theorem ssonunii

Description: The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of Enderton p. 193. (Contributed by NM, 20-Sep-2003)

Ref Expression
Hypothesis ssonuni.1 AV
Assertion ssonunii AOnAOn

Proof

Step Hyp Ref Expression
1 ssonuni.1 AV
2 ssonuni AVAOnAOn
3 1 2 ax-mp AOnAOn