Theorem nndomog

Description: Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo when both are natural numbers. (Contributed by NM, 17-Jun-1998) Generalize from nndomo . (Revised by RP, 5-Nov-2023) Avoid ax-pow . (Revised by BTernaryTau, 29-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		nnfi	|- ( A e. _om -> A e. Fin )
2		domnsymfi	|- ( ( A e. Fin /\ A ~<_ B ) -> -. B ~< A )
3	1 2	sylan	|- ( ( A e. _om /\ A ~<_ B ) -> -. B ~< A )
4	3	ex	|- ( A e. _om -> ( A ~<_ B -> -. B ~< A ) )
5		php2	|- ( ( A e. _om /\ B C. A ) -> B ~< A )
6	5	ex	|- ( A e. _om -> ( B C. A -> B ~< A ) )
7	4 6	nsyld	|- ( A e. _om -> ( A ~<_ B -> -. B C. A ) )
8	7	adantr	|- ( ( A e. _om /\ B e. On ) -> ( A ~<_ B -> -. B C. A ) )
9		nnord	|- ( A e. _om -> Ord A )
10		eloni	|- ( B e. On -> Ord B )
11		ordtri1	|- ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) )
12		ordelpss	|- ( ( Ord B /\ Ord A ) -> ( B e. A <-> B C. A ) )
13	12	ancoms	|- ( ( Ord A /\ Ord B ) -> ( B e. A <-> B C. A ) )
14	13	notbid	|- ( ( Ord A /\ Ord B ) -> ( -. B e. A <-> -. B C. A ) )
15	11 14	bitrd	|- ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B C. A ) )
16	9 10 15	syl2an	|- ( ( A e. _om /\ B e. On ) -> ( A C_ B <-> -. B C. A ) )
17	8 16	sylibrd	|- ( ( A e. _om /\ B e. On ) -> ( A ~<_ B -> A C_ B ) )
18		ssdomfi2	|- ( ( A e. Fin /\ B e. On /\ A C_ B ) -> A ~<_ B )
19	18	3expia	|- ( ( A e. Fin /\ B e. On ) -> ( A C_ B -> A ~<_ B ) )
20	1 19	sylan	|- ( ( A e. _om /\ B e. On ) -> ( A C_ B -> A ~<_ B ) )
21	17 20	impbid	|- ( ( A e. _om /\ B e. On ) -> ( A ~<_ B <-> A C_ B ) )