Theorem nnuni

Description: The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Assertion	nnuni	⊢ ( 𝐴 ∈ ω → ∪ 𝐴 ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		nn0suc	⊢ ( 𝐴 ∈ ω → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) )
2		unieq	⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∪ ∅ )
3		uni0	⊢ ∪ ∅ = ∅
4	2 3	eqtrdi	⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∅ )
5		peano1	⊢ ∅ ∈ ω
6	4 5	eqeltrdi	⊢ ( 𝐴 = ∅ → ∪ 𝐴 ∈ ω )
7		nnord	⊢ ( 𝑥 ∈ ω → Ord 𝑥 )
8		ordunisuc	⊢ ( Ord 𝑥 → ∪ suc 𝑥 = 𝑥 )
9	7 8	syl	⊢ ( 𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥 )
10		id	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ ω )
11	9 10	eqeltrd	⊢ ( 𝑥 ∈ ω → ∪ suc 𝑥 ∈ ω )
12		unieq	⊢ ( 𝐴 = suc 𝑥 → ∪ 𝐴 = ∪ suc 𝑥 )
13	12	eleq1d	⊢ ( 𝐴 = suc 𝑥 → ( ∪ 𝐴 ∈ ω ↔ ∪ suc 𝑥 ∈ ω ) )
14	11 13	syl5ibrcom	⊢ ( 𝑥 ∈ ω → ( 𝐴 = suc 𝑥 → ∪ 𝐴 ∈ ω ) )
15	14	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 → ∪ 𝐴 ∈ ω )
16	6 15	jaoi	⊢ ( ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) → ∪ 𝐴 ∈ ω )
17	1 16	syl	⊢ ( 𝐴 ∈ ω → ∪ 𝐴 ∈ ω )