Metamath Proof Explorer

Theorem ontri1

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

Ref Expression
Assertion ontri1 
|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> -. B e. A ) )

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( A e. On -> Ord A )
2 eloni 
 |-  ( B e. On -> Ord B )
3 ordtri1 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) )
4 1 2 3 syl2an 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> -. B e. A ) )