Metamath Proof Explorer


Theorem ordtri1

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ordtri1 Ord A Ord B A B ¬ B A

Proof

Step Hyp Ref Expression
1 ordsseleq Ord A Ord B A B A B A = B
2 ordn2lp Ord A ¬ A B B A
3 imnan A B ¬ B A ¬ A B B A
4 2 3 sylibr Ord A A B ¬ B A
5 ordirr Ord B ¬ B B
6 eleq2 A = B B A B B
7 6 notbid A = B ¬ B A ¬ B B
8 5 7 syl5ibrcom Ord B A = B ¬ B A
9 4 8 jaao Ord A Ord B A B A = B ¬ B A
10 ordtri3or Ord A Ord B A B A = B B A
11 df-3or A B A = B B A A B A = B B A
12 10 11 sylib Ord A Ord B A B A = B B A
13 12 orcomd Ord A Ord B B A A B A = B
14 13 ord Ord A Ord B ¬ B A A B A = B
15 9 14 impbid Ord A Ord B A B A = B ¬ B A
16 1 15 bitrd Ord A Ord B A B ¬ B A