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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		php5	⊢ ( 𝐵 ∈ ω → ¬ 𝐵 ≈ suc 𝐵 )
2	1	ad2antlr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ≈ suc 𝐵 )
3		enen1	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ≈ suc 𝐵 ↔ 𝐵 ≈ suc 𝐵 ) )
4	3	adantl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ( 𝐴 ≈ suc 𝐵 ↔ 𝐵 ≈ suc 𝐵 ) )
5	2 4	mtbird	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐴 ≈ suc 𝐵 )
6		peano2	⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ ω )
7		sssucid	⊢ 𝐵 ⊆ suc 𝐵
8		ssdomg	⊢ ( suc 𝐵 ∈ ω → ( 𝐵 ⊆ suc 𝐵 → 𝐵 ≼ suc 𝐵 ) )
9	6 7 8	mpisyl	⊢ ( 𝐵 ∈ ω → 𝐵 ≼ suc 𝐵 )
10		endomtr	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ≼ suc 𝐵 ) → 𝐴 ≼ suc 𝐵 )
11	9 10	sylan2	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝐴 ≼ suc 𝐵 )
12	11	ancoms	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ≼ suc 𝐵 )
13	12	a1d	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵 ) → ( ω ⊆ 𝐴 → 𝐴 ≼ suc 𝐵 ) )
14	13	adantll	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ( ω ⊆ 𝐴 → 𝐴 ≼ suc 𝐵 ) )
15		ssel	⊢ ( ω ⊆ 𝐴 → ( 𝐵 ∈ ω → 𝐵 ∈ 𝐴 ) )
16	15	com12	⊢ ( 𝐵 ∈ ω → ( ω ⊆ 𝐴 → 𝐵 ∈ 𝐴 ) )
17	16	adantr	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ On ) → ( ω ⊆ 𝐴 → 𝐵 ∈ 𝐴 ) )
18		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
19		ordelsuc	⊢ ( ( 𝐵 ∈ ω ∧ Ord 𝐴 ) → ( 𝐵 ∈ 𝐴 ↔ suc 𝐵 ⊆ 𝐴 ) )
20	18 19	sylan2	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ 𝐴 ↔ suc 𝐵 ⊆ 𝐴 ) )
21	17 20	sylibd	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ On ) → ( ω ⊆ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )
22		ssdomg	⊢ ( 𝐴 ∈ On → ( suc 𝐵 ⊆ 𝐴 → suc 𝐵 ≼ 𝐴 ) )
23	22	adantl	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ On ) → ( suc 𝐵 ⊆ 𝐴 → suc 𝐵 ≼ 𝐴 ) )
24	21 23	syld	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ On ) → ( ω ⊆ 𝐴 → suc 𝐵 ≼ 𝐴 ) )
25	24	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ω ⊆ 𝐴 → suc 𝐵 ≼ 𝐴 ) )
26	25	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ( ω ⊆ 𝐴 → suc 𝐵 ≼ 𝐴 ) )
27	14 26	jcad	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ( ω ⊆ 𝐴 → ( 𝐴 ≼ suc 𝐵 ∧ suc 𝐵 ≼ 𝐴 ) ) )
28		sbth	⊢ ( ( 𝐴 ≼ suc 𝐵 ∧ suc 𝐵 ≼ 𝐴 ) → 𝐴 ≈ suc 𝐵 )
29	27 28	syl6	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ( ω ⊆ 𝐴 → 𝐴 ≈ suc 𝐵 ) )
30	5 29	mtod	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ¬ ω ⊆ 𝐴 )
31		ordom	⊢ Ord ω
32		ordtri1	⊢ ( ( Ord ω ∧ Ord 𝐴 ) → ( ω ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ω ) )
33	31 18 32	sylancr	⊢ ( 𝐴 ∈ On → ( ω ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ω ) )
34	33	con2bid	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ ω ↔ ¬ ω ⊆ 𝐴 ) )
35	34	ad2antrr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ( 𝐴 ∈ ω ↔ ¬ ω ⊆ 𝐴 ) )
36	30 35	mpbird	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ ω )
37		simplr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ∈ ω )
38	36 37	jca	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) )
39		nneneq	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) )
40	39	biimpa	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → 𝐴 = 𝐵 )
41	38 40	sylancom	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) ∧ 𝐴 ≈ 𝐵 ) → 𝐴 = 𝐵 )
42	41	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 → 𝐴 = 𝐵 ) )
43		eqeng	⊢ ( 𝐴 ∈ On → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )
44	43	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )
45	42 44	impbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) )