Metamath Proof Explorer


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)

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

Proof

Step Hyp Ref Expression
1 php2
 |-  ( ( A e. _om /\ B C. A ) -> B ~< A )
2 1 ex
 |-  ( A e. _om -> ( B C. A -> B ~< A ) )
3 domnsym
 |-  ( A ~<_ B -> -. B ~< A )
4 2 3 nsyli
 |-  ( A e. _om -> ( A ~<_ B -> -. B C. A ) )
5 4 adantr
 |-  ( ( A e. _om /\ B e. On ) -> ( A ~<_ B -> -. B C. A ) )
6 nnord
 |-  ( A e. _om -> Ord A )
7 eloni
 |-  ( B e. On -> Ord B )
8 ordtri1
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) )
9 ordelpss
 |-  ( ( Ord B /\ Ord A ) -> ( B e. A <-> B C. A ) )
10 9 ancoms
 |-  ( ( Ord A /\ Ord B ) -> ( B e. A <-> B C. A ) )
11 10 notbid
 |-  ( ( Ord A /\ Ord B ) -> ( -. B e. A <-> -. B C. A ) )
12 8 11 bitrd
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B C. A ) )
13 6 7 12 syl2an
 |-  ( ( A e. _om /\ B e. On ) -> ( A C_ B <-> -. B C. A ) )
14 5 13 sylibrd
 |-  ( ( A e. _om /\ B e. On ) -> ( A ~<_ B -> A C_ B ) )
15 ssdomg
 |-  ( B e. On -> ( A C_ B -> A ~<_ B ) )
16 15 adantl
 |-  ( ( A e. _om /\ B e. On ) -> ( A C_ B -> A ~<_ B ) )
17 14 16 impbid
 |-  ( ( A e. _om /\ B e. On ) -> ( A ~<_ B <-> A C_ B ) )