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