Metamath Proof Explorer

Theorem nndomo

Description: Cardinal ordering agrees with natural number ordering. Example 3 of Enderton p. 146. (Contributed by NM, 17-Jun-1998)

Ref Expression
Assertion nndomo 
|- ( ( A e. _om /\ B e. _om ) -> ( A ~<_ B <-> A C_ B ) )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( B e. _om -> B e. On )
2 nndomog 
 |-  ( ( A e. _om /\ B e. On ) -> ( A ~<_ B <-> A C_ B ) )
3 1 2 sylan2 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ~<_ B <-> A C_ B ) )