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 C_ B <-> -. B e. A ) )

Proof

Step Hyp Ref Expression
1 ordsseleq 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
2 ordn2lp 
 |-  ( Ord A -> -. ( A e. B /\ B e. A ) )
3 imnan 
 |-  ( ( A e. B -> -. B e. A ) <-> -. ( A e. B /\ B e. A ) )
4 2 3 sylibr 
 |-  ( Ord A -> ( A e. B -> -. B e. A ) )
5 ordirr 
 |-  ( Ord B -> -. B e. B )
6 eleq2 
 |-  ( A = B -> ( B e. A <-> B e. B ) )
7 6 notbid 
 |-  ( A = B -> ( -. B e. A <-> -. B e. B ) )
8 5 7 syl5ibrcom 
 |-  ( Ord B -> ( A = B -> -. B e. A ) )
9 4 8 jaao 
 |-  ( ( Ord A /\ Ord B ) -> ( ( A e. B \/ A = B ) -> -. B e. A ) )
10 ordtri3or 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B \/ A = B \/ B e. A ) )
11 df-3or 
 |-  ( ( A e. B \/ A = B \/ B e. A ) <-> ( ( A e. B \/ A = B ) \/ B e. A ) )
12 10 11 sylib 
 |-  ( ( Ord A /\ Ord B ) -> ( ( A e. B \/ A = B ) \/ B e. A ) )
13 12 orcomd 
 |-  ( ( Ord A /\ Ord B ) -> ( B e. A \/ ( A e. B \/ A = B ) ) )
14 13 ord 
 |-  ( ( Ord A /\ Ord B ) -> ( -. B e. A -> ( A e. B \/ A = B ) ) )
15 9 14 impbid 
 |-  ( ( Ord A /\ Ord B ) -> ( ( A e. B \/ A = B ) <-> -. B e. A ) )
16 1 15 bitrd 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) )