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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 ) ∈ ω )

Proof

Step Hyp Ref Expression
1 ssequn1 ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = 𝐵 )
2 eleq1a ( 𝐵 ∈ ω → ( ( 𝐴𝐵 ) = 𝐵 → ( 𝐴𝐵 ) ∈ ω ) )
3 2 adantl ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴𝐵 ) = 𝐵 → ( 𝐴𝐵 ) ∈ ω ) )
4 1 3 biimtrid ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐴𝐵 ) ∈ ω ) )
5 ssequn2 ( 𝐵𝐴 ↔ ( 𝐴𝐵 ) = 𝐴 )
6 eleq1a ( 𝐴 ∈ ω → ( ( 𝐴𝐵 ) = 𝐴 → ( 𝐴𝐵 ) ∈ ω ) )
7 6 adantr ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴𝐵 ) = 𝐴 → ( 𝐴𝐵 ) ∈ ω ) )
8 5 7 biimtrid ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵𝐴 → ( 𝐴𝐵 ) ∈ ω ) )
9 nnord ( 𝐴 ∈ ω → Ord 𝐴 )
10 nnord ( 𝐵 ∈ ω → Ord 𝐵 )
11 ordtri2or2 ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴𝐵𝐵𝐴 ) )
12 9 10 11 syl2an ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵𝐵𝐴 ) )
13 4 8 12 mpjaod ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 ) ∈ ω )