Metamath Proof Explorer

Theorem ssonuni

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

Ref Expression
Assertion ssonuni 
|- ( A e. V -> ( A C_ On -> U. A e. On ) )

Proof

Step Hyp Ref Expression
1 ssorduni 
 |-  ( A C_ On -> Ord U. A )
2 uniexg 
 |-  ( A e. V -> U. A e. _V )
3 elong 
 |-  ( U. A e. _V -> ( U. A e. On <-> Ord U. A ) )
4 2 3 syl 
 |-  ( A e. V -> ( U. A e. On <-> Ord U. A ) )
5 1 4 syl5ibr 
 |-  ( A e. V -> ( A C_ On -> U. A e. On ) )