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

Proof

Step	Hyp	Ref	Expression
1		endom	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵 )
2		nnfi	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ Fin )
3		domfi	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ∈ Fin )
4		simpr	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≼ 𝐵 )
5	3 4	jca	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) )
6		domnsymfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )
7	6	ex	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴 ) )
8		php3	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≺ 𝐴 )
9	8	ex	⊢ ( 𝐴 ∈ Fin → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴 ) )
10	7 9	nsyld	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ⊊ 𝐴 ) )
11	10	adantl	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ Fin ) → ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ⊊ 𝐴 ) )
12	11	expimpd	⊢ ( 𝐵 ∈ ω → ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ¬ 𝐵 ⊊ 𝐴 ) )
13	5 12	syl5	⊢ ( 𝐵 ∈ ω → ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ¬ 𝐵 ⊊ 𝐴 ) )
14	2 13	mpand	⊢ ( 𝐵 ∈ ω → ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ⊊ 𝐴 ) )
15	14	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ⊊ 𝐴 ) )
16		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
17		nnord	⊢ ( 𝐵 ∈ ω → Ord 𝐵 )
18		ordtri1	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
19		ordelpss	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴 ) )
20	19	ancoms	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴 ) )
21	20	notbid	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ⊊ 𝐴 ) )
22	18 21	bitrd	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ⊊ 𝐴 ) )
23	16 17 22	syl2an	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ⊊ 𝐴 ) )
24	15 23	sylibrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ≼ 𝐵 → 𝐴 ⊆ 𝐵 ) )
25	1 24	syl5	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 → 𝐴 ⊆ 𝐵 ) )
26	25	3impia	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ⊆ 𝐵 )
27		ensymfib	⊢ ( 𝐵 ∈ Fin → ( 𝐵 ≈ 𝐴 ↔ 𝐴 ≈ 𝐵 ) )
28	2 27	syl	⊢ ( 𝐵 ∈ ω → ( 𝐵 ≈ 𝐴 ↔ 𝐴 ≈ 𝐵 ) )
29		endom	⊢ ( 𝐵 ≈ 𝐴 → 𝐵 ≼ 𝐴 )
30	28 29	syl6bir	⊢ ( 𝐵 ∈ ω → ( 𝐴 ≈ 𝐵 → 𝐵 ≼ 𝐴 ) )
31	30	imp	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ≼ 𝐴 )
32	31	3adant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ≼ 𝐴 )
33		nndomog	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ On ) → ( 𝐵 ≼ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
34	33	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐵 ≼ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
35	34	biimp3a	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ⊆ 𝐴 )
36	32 35	syld3an3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ⊆ 𝐴 )
37	26 36	eqssd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵 ) → 𝐴 = 𝐵 )
38	37	3expia	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 → 𝐴 = 𝐵 ) )
39		enrefnn	⊢ ( 𝐵 ∈ ω → 𝐵 ≈ 𝐵 )
40		breq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐵 ) )
41	39 40	syl5ibrcom	⊢ ( 𝐵 ∈ ω → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )
42	41	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )
43	38 42	impbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) )