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 ∈ On ∧ B ∈ ω → A ≈ B ↔ A = B

Proof

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