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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )

Proof

Step	Hyp	Ref	Expression
1		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
2		uniexg	⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )
3		elong	⊢ ( ∪ 𝐴 ∈ V → ( ∪ 𝐴 ∈ On ↔ Ord ∪ 𝐴 ) )
4	2 3	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝐴 ∈ On ↔ Ord ∪ 𝐴 ) )
5	1 4	syl5ibr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )