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 ω