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