Theorem nnunifi

Description: The union (supremum) of a finite set of finite ordinals is a finite ordinal. (Contributed by Stefan O'Rear, 5-Nov-2014)

	Ref	Expression
Assertion	nnunifi	⊢ ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) → ∪ 𝑆 ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		unieq	⊢ ( 𝑆 = ∅ → ∪ 𝑆 = ∪ ∅ )
2		uni0	⊢ ∪ ∅ = ∅
3		peano1	⊢ ∅ ∈ ω
4	2 3	eqeltri	⊢ ∪ ∅ ∈ ω
5	1 4	eqeltrdi	⊢ ( 𝑆 = ∅ → ∪ 𝑆 ∈ ω )
6	5	adantl	⊢ ( ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) ∧ 𝑆 = ∅ ) → ∪ 𝑆 ∈ ω )
7		simpll	⊢ ( ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ⊆ ω )
8		omsson	⊢ ω ⊆ On
9	7 8	sstrdi	⊢ ( ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ⊆ On )
10		simplr	⊢ ( ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ∈ Fin )
11		simpr	⊢ ( ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ≠ ∅ )
12		ordunifi	⊢ ( ( 𝑆 ⊆ On ∧ 𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ) → ∪ 𝑆 ∈ 𝑆 )
13	9 10 11 12	syl3anc	⊢ ( ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) ∧ 𝑆 ≠ ∅ ) → ∪ 𝑆 ∈ 𝑆 )
14	7 13	sseldd	⊢ ( ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) ∧ 𝑆 ≠ ∅ ) → ∪ 𝑆 ∈ ω )
15	6 14	pm2.61dane	⊢ ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) → ∪ 𝑆 ∈ ω )