Metamath Proof Explorer


Theorem ordtri2

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995)

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

Proof

Step Hyp Ref Expression
1 ordsseleq Ord B Ord A B A B A B = A
2 eqcom B = A A = B
3 2 orbi2i B A B = A B A A = B
4 orcom B A A = B A = B B A
5 3 4 bitri B A B = A A = B B A
6 1 5 bitrdi Ord B Ord A B A A = B B A
7 ordtri1 Ord B Ord A B A ¬ A B
8 6 7 bitr3d Ord B Ord A A = B B A ¬ A B
9 8 ancoms Ord A Ord B A = B B A ¬ A B
10 9 con2bid Ord A Ord B A B ¬ A = B B A