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

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