This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnsdomo

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

Ref Expression
Assertion nnsdomo 
|- ( ( A e. _om /\ B e. _om ) -> ( A ~< B <-> A C. B ) )

Proof

Step Hyp Ref Expression
1 nndomo 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ~<_ B <-> A C_ B ) )
2 nneneq 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ~~ B <-> A = B ) )
3 2 notbid 
 |-  ( ( A e. _om /\ B e. _om ) -> ( -. A ~~ B <-> -. A = B ) )
4 1 3 anbi12d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A ~<_ B /\ -. A ~~ B ) <-> ( A C_ B /\ -. A = B ) ) )
5 brsdom 
 |-  ( A ~< B <-> ( A ~<_ B /\ -. A ~~ B ) )
6 dfpss2 
 |-  ( A C. B <-> ( A C_ B /\ -. A = B ) )
7 4 5 6 3bitr4g 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ~< B <-> A C. B ) )