Theorem orduni

Description: The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003)

	Ref	Expression
Assertion	orduni	$$⊢\mathrm{Ord}A\to \mathrm{Ord}\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		ordsson	$$⊢\mathrm{Ord}A\to A\subseteq \mathrm{On}$$
2		ssorduni	$$⊢A\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup A$$
3	1 2	syl	$$⊢\mathrm{Ord}A\to \mathrm{Ord}\bigcup A$$