Metamath Proof Explorer

Theorem onuni

Description: The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006)

Ref Expression
Assertion onuni 
|- ( A e. On -> U. A e. On )

Proof

Step Hyp Ref Expression
1 onss 
 |-  ( A e. On -> A C_ On )
2 ssonuni 
 |-  ( A e. On -> ( A C_ On -> U. A e. On ) )
3 1 2 mpd 
 |-  ( A e. On -> U. A e. On )