Theorem ssonunii

Description: The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of Enderton p. 193. (Contributed by NM, 20-Sep-2003)

	Ref	Expression
Hypothesis	ssonuni.1	⊢ 𝐴 ∈ V
Assertion	ssonunii	⊢ ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		ssonuni.1	⊢ 𝐴 ∈ V
2		ssonuni	⊢ ( 𝐴 ∈ V → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )
3	1 2	ax-mp	⊢ ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On )