Metamath Proof Explorer

Theorem onun2

Description: The union of two ordinals is an ordinal. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Assertion onun2 ⊢ A ∈ On ∧ B ∈ On → A ∪ B ∈ On

Proof

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