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)

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

Proof

Step	Hyp	Ref	Expression
1		php5	|- ( B e. _om -> -. B ~~ suc B )
2	1	ad2antlr	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> -. B ~~ suc B )
3		enen1	|- ( A ~~ B -> ( A ~~ suc B <-> B ~~ suc B ) )
4	3	adantl	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> ( A ~~ suc B <-> B ~~ suc B ) )
5	2 4	mtbird	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> -. A ~~ suc B )
6		peano2	|- ( B e. _om -> suc B e. _om )
7		sssucid	|- B C_ suc B
8		ssdomg	|- ( suc B e. _om -> ( B C_ suc B -> B ~<_ suc B ) )
9	6 7 8	mpisyl	|- ( B e. _om -> B ~<_ suc B )
10		endomtr	|- ( ( A ~~ B /\ B ~<_ suc B ) -> A ~<_ suc B )
11	9 10	sylan2	|- ( ( A ~~ B /\ B e. _om ) -> A ~<_ suc B )
12	11	ancoms	|- ( ( B e. _om /\ A ~~ B ) -> A ~<_ suc B )
13	12	a1d	|- ( ( B e. _om /\ A ~~ B ) -> ( _om C_ A -> A ~<_ suc B ) )
14	13	adantll	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> ( _om C_ A -> A ~<_ suc B ) )
15		ssel	|- ( _om C_ A -> ( B e. _om -> B e. A ) )
16	15	com12	|- ( B e. _om -> ( _om C_ A -> B e. A ) )
17	16	adantr	|- ( ( B e. _om /\ A e. On ) -> ( _om C_ A -> B e. A ) )
18		eloni	|- ( A e. On -> Ord A )
19		ordelsuc	|- ( ( B e. _om /\ Ord A ) -> ( B e. A <-> suc B C_ A ) )
20	18 19	sylan2	|- ( ( B e. _om /\ A e. On ) -> ( B e. A <-> suc B C_ A ) )
21	17 20	sylibd	|- ( ( B e. _om /\ A e. On ) -> ( _om C_ A -> suc B C_ A ) )
22		ssdomg	|- ( A e. On -> ( suc B C_ A -> suc B ~<_ A ) )
23	22	adantl	|- ( ( B e. _om /\ A e. On ) -> ( suc B C_ A -> suc B ~<_ A ) )
24	21 23	syld	|- ( ( B e. _om /\ A e. On ) -> ( _om C_ A -> suc B ~<_ A ) )
25	24	ancoms	|- ( ( A e. On /\ B e. _om ) -> ( _om C_ A -> suc B ~<_ A ) )
26	25	adantr	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> ( _om C_ A -> suc B ~<_ A ) )
27	14 26	jcad	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> ( _om C_ A -> ( A ~<_ suc B /\ suc B ~<_ A ) ) )
28		sbth	|- ( ( A ~<_ suc B /\ suc B ~<_ A ) -> A ~~ suc B )
29	27 28	syl6	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> ( _om C_ A -> A ~~ suc B ) )
30	5 29	mtod	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> -. _om C_ A )
31		ordom	|- Ord _om
32		ordtri1	|- ( ( Ord _om /\ Ord A ) -> ( _om C_ A <-> -. A e. _om ) )
33	31 18 32	sylancr	|- ( A e. On -> ( _om C_ A <-> -. A e. _om ) )
34	33	con2bid	|- ( A e. On -> ( A e. _om <-> -. _om C_ A ) )
35	34	ad2antrr	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> ( A e. _om <-> -. _om C_ A ) )
36	30 35	mpbird	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> A e. _om )
37		simplr	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> B e. _om )
38	36 37	jca	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> ( A e. _om /\ B e. _om ) )
39		nneneq	|- ( ( A e. _om /\ B e. _om ) -> ( A ~~ B <-> A = B ) )
40	39	biimpa	|- ( ( ( A e. _om /\ B e. _om ) /\ A ~~ B ) -> A = B )
41	38 40	sylancom	|- ( ( ( A e. On /\ B e. _om ) /\ A ~~ B ) -> A = B )
42	41	ex	|- ( ( A e. On /\ B e. _om ) -> ( A ~~ B -> A = B ) )
43		eqeng	|- ( A e. On -> ( A = B -> A ~~ B ) )
44	43	adantr	|- ( ( A e. On /\ B e. _om ) -> ( A = B -> A ~~ B ) )
45	42 44	impbid	|- ( ( A e. On /\ B e. _om ) -> ( A ~~ B <-> A = B ) )