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 ) )