Metamath Proof Explorer


Theorem nnsdomo

Description: Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998)

Ref Expression
Assertion nnsdomo A ω B ω A B A B

Proof

Step Hyp Ref Expression
1 nndomo A ω B ω A B A B
2 nneneq A ω B ω A B A = B
3 2 notbid A ω B ω ¬ A B ¬ A = B
4 1 3 anbi12d A ω B ω A B ¬ A B A B ¬ A = B
5 brsdom A B A B ¬ A B
6 dfpss2 A B A B ¬ A = B
7 4 5 6 3bitr4g A ω B ω A B A B