Theorem onuni

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

	Ref	Expression
Assertion	onuni	⊢ ( 𝐴 ∈ On → ∪ 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		onss	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
2		ssonuni	⊢ ( 𝐴 ∈ On → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )
3	1 2	mpd	⊢ ( 𝐴 ∈ On → ∪ 𝐴 ∈ On )