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