Metamath Proof Explorer


Theorem ordtri3

Description: A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by JJ, 24-Sep-2021)

Ref Expression
Assertion ordtri3 Ord A Ord B A = B ¬ A B B A

Proof

Step Hyp Ref Expression
1 ordirr Ord B ¬ B B
2 1 adantl Ord A Ord B ¬ B B
3 eleq2 A = B B A B B
4 3 notbid A = B ¬ B A ¬ B B
5 2 4 syl5ibrcom Ord A Ord B A = B ¬ B A
6 5 pm4.71d Ord A Ord B A = B A = B ¬ B A
7 pm5.61 A = B B A ¬ B A A = B ¬ B A
8 pm4.52 A = B B A ¬ B A ¬ ¬ A = B B A B A
9 7 8 bitr3i A = B ¬ B A ¬ ¬ A = B B A B A
10 6 9 syl6bb Ord A Ord B A = B ¬ ¬ A = B B A B A
11 ordtri2 Ord A Ord B A B ¬ A = B B A
12 11 orbi1d Ord A Ord B A B B A ¬ A = B B A B A
13 12 notbid Ord A Ord B ¬ A B B A ¬ ¬ A = B B A B A
14 10 13 bitr4d Ord A Ord B A = B ¬ A B B A