Metamath Proof Explorer


Theorem ordtri2or2

Description: A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003)

Ref Expression
Assertion ordtri2or2 OrdAOrdBABBA

Proof

Step Hyp Ref Expression
1 ordtri2or OrdAOrdBABBA
2 ordelss OrdBABAB
3 2 ex OrdBABAB
4 3 orim1d OrdBABBAABBA
5 4 adantl OrdAOrdBABBAABBA
6 1 5 mpd OrdAOrdBABBA