This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ∪ 𝑆 ∈ ω )