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\in V\to \left(A\subseteq \mathrm{On}\to \bigcup A\in \mathrm{On}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssorduni	$$⊢A\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup A$$
2		uniexg	$$⊢A\in V\to \bigcup A\in \mathrm{V}$$
3		elong	$$⊢\bigcup A\in \mathrm{V}\to \left(\bigcup A\in \mathrm{On}\leftrightarrow \mathrm{Ord}\bigcup A\right)$$
4	2 3	syl	$$⊢A\in V\to \left(\bigcup A\in \mathrm{On}\leftrightarrow \mathrm{Ord}\bigcup A\right)$$
5	1 4	syl5ibr	$$⊢A\in V\to \left(A\subseteq \mathrm{On}\to \bigcup A\in \mathrm{On}\right)$$