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

Metamath Proof Explorer

Theorem onomeneq

Description: An ordinal number equinumerous to a natural number is equal to it. Proposition 10.22 of TakeutiZaring p. 90 and its converse. (Contributed by NM, 26-Jul-2004) Avoid ax-pow . (Revised by BTernaryTau, 2-Dec-2024)

Ref Expression
Assertion onomeneq 
|- ( ( A e. On /\ B e. _om ) -> ( A ~~ B <-> A = B ) )

Proof

Step Hyp Ref Expression
1 endom 
 |-  ( A ~~ B -> A ~<_ B )
2 nnfi 
 |-  ( B e. _om -> B e. Fin )
3 domfi 
 |-  ( ( B e. Fin /\ A ~<_ B ) -> A e. Fin )
4 simpr 
 |-  ( ( B e. Fin /\ A ~<_ B ) -> A ~<_ B )
5 3 4 jca 
 |-  ( ( B e. Fin /\ A ~<_ B ) -> ( A e. Fin /\ A ~<_ B ) )
6 domnsymfi 
 |-  ( ( A e. Fin /\ A ~<_ B ) -> -. B ~< A )
7 6 ex 
 |-  ( A e. Fin -> ( A ~<_ B -> -. B ~< A ) )
8 php3 
 |-  ( ( A e. Fin /\ B C. A ) -> B ~< A )
9 8 ex 
 |-  ( A e. Fin -> ( B C. A -> B ~< A ) )
10 7 9 nsyld 
 |-  ( A e. Fin -> ( A ~<_ B -> -. B C. A ) )
11 10 adantl 
 |-  ( ( B e. _om /\ A e. Fin ) -> ( A ~<_ B -> -. B C. A ) )
12 11 expimpd 
 |-  ( B e. _om -> ( ( A e. Fin /\ A ~<_ B ) -> -. B C. A ) )
13 5 12 syl5 
 |-  ( B e. _om -> ( ( B e. Fin /\ A ~<_ B ) -> -. B C. A ) )
14 2 13 mpand 
 |-  ( B e. _om -> ( A ~<_ B -> -. B C. A ) )
15 14 adantl 
 |-  ( ( A e. On /\ B e. _om ) -> ( A ~<_ B -> -. B C. A ) )
16 eloni 
 |-  ( A e. On -> Ord A )
17 nnord 
 |-  ( B e. _om -> Ord B )
18 ordtri1 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) )
19 ordelpss 
 |-  ( ( Ord B /\ Ord A ) -> ( B e. A <-> B C. A ) )
20 19 ancoms 
 |-  ( ( Ord A /\ Ord B ) -> ( B e. A <-> B C. A ) )
21 20 notbid 
 |-  ( ( Ord A /\ Ord B ) -> ( -. B e. A <-> -. B C. A ) )
22 18 21 bitrd 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B C. A ) )
23 16 17 22 syl2an 
 |-  ( ( A e. On /\ B e. _om ) -> ( A C_ B <-> -. B C. A ) )
24 15 23 sylibrd 
 |-  ( ( A e. On /\ B e. _om ) -> ( A ~<_ B -> A C_ B ) )
25 1 24 syl5 
 |-  ( ( A e. On /\ B e. _om ) -> ( A ~~ B -> A C_ B ) )
26 25 3impia 
 |-  ( ( A e. On /\ B e. _om /\ A ~~ B ) -> A C_ B )
27 ensymfib 
 |-  ( B e. Fin -> ( B ~~ A <-> A ~~ B ) )
28 2 27 syl 
 |-  ( B e. _om -> ( B ~~ A <-> A ~~ B ) )
29 endom 
 |-  ( B ~~ A -> B ~<_ A )
30 28 29 biimtrrdi 
 |-  ( B e. _om -> ( A ~~ B -> B ~<_ A ) )
31 30 imp 
 |-  ( ( B e. _om /\ A ~~ B ) -> B ~<_ A )
32 31 3adant1 
 |-  ( ( A e. On /\ B e. _om /\ A ~~ B ) -> B ~<_ A )
33 nndomog 
 |-  ( ( B e. _om /\ A e. On ) -> ( B ~<_ A <-> B C_ A ) )
34 33 ancoms 
 |-  ( ( A e. On /\ B e. _om ) -> ( B ~<_ A <-> B C_ A ) )
35 34 biimp3a 
 |-  ( ( A e. On /\ B e. _om /\ B ~<_ A ) -> B C_ A )
36 32 35 syld3an3 
 |-  ( ( A e. On /\ B e. _om /\ A ~~ B ) -> B C_ A )
37 26 36 eqssd 
 |-  ( ( A e. On /\ B e. _om /\ A ~~ B ) -> A = B )
38 37 3expia 
 |-  ( ( A e. On /\ B e. _om ) -> ( A ~~ B -> A = B ) )
39 enrefnn 
 |-  ( B e. _om -> B ~~ B )
40 breq1 
 |-  ( A = B -> ( A ~~ B <-> B ~~ B ) )
41 39 40 syl5ibrcom 
 |-  ( B e. _om -> ( A = B -> A ~~ B ) )
42 41 adantl 
 |-  ( ( A e. On /\ B e. _om ) -> ( A = B -> A ~~ B ) )
43 38 42 impbid 
 |-  ( ( A e. On /\ B e. _om ) -> ( A ~~ B <-> A = B ) )