Metamath Proof Explorer

Theorem omun

Description: The union of two finite ordinals is a finite ordinal. (Contributed by Scott Fenton, 15-Mar-2025)

Ref Expression
Assertion omun ⊢ A ∈ ω ∧ B ∈ ω → A ∪ B ∈ ω

Proof

Step Hyp Ref Expression
1 ssequn1 ⊢ A ⊆ B ↔ A ∪ B = B
2 eleq1a ⊢ B ∈ ω → A ∪ B = B → A ∪ B ∈ ω
3 2 adantl ⊢ A ∈ ω ∧ B ∈ ω → A ∪ B = B → A ∪ B ∈ ω
4 1 3 biimtrid ⊢ A ∈ ω ∧ B ∈ ω → A ⊆ B → A ∪ B ∈ ω
5 ssequn2 ⊢ B ⊆ A ↔ A ∪ B = A
6 eleq1a ⊢ A ∈ ω → A ∪ B = A → A ∪ B ∈ ω
7 6 adantr ⊢ A ∈ ω ∧ B ∈ ω → A ∪ B = A → A ∪ B ∈ ω
8 5 7 biimtrid ⊢ A ∈ ω ∧ B ∈ ω → B ⊆ A → A ∪ B ∈ ω
9 nnord ⊢ A ∈ ω → Ord ⁡ A
10 nnord ⊢ B ∈ ω → Ord ⁡ B
11 ordtri2or2 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ∨ B ⊆ A
12 9 10 11 syl2an ⊢ A ∈ ω ∧ B ∈ ω → A ⊆ B ∨ B ⊆ A
13 4 8 12 mpjaod ⊢ A ∈ ω ∧ B ∈ ω → A ∪ B ∈ ω