This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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