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 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	imbitrrid	|- ( A e. V -> ( A C_ On -> U. A e. On ) )