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 syl5bi 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 syl5bi 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