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ωBωABAB

Proof

Step Hyp Ref Expression
1 nnon BωBOn
2 nndomog AωBOnABAB
3 1 2 sylan2 AωBωABAB