Metamath Proof Explorer

Theorem nneneq

Description: Two equinumerous natural numbers are equal. Proposition 10.20 of TakeutiZaring p. 90 and its converse. Also compare Corollary 6E of Enderton p. 136. (Contributed by NM, 28-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 11-Nov-2024)

Ref Expression
Assertion nneneq ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ≈ 𝑧 ↔ ∅ ≈ 𝑧 ) )
2 eqeq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 = 𝑧 ↔ ∅ = 𝑧 ) )
3 1 2 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ≈ 𝑧 → 𝑥 = 𝑧 ) ↔ ( ∅ ≈ 𝑧 → ∅ = 𝑧 ) ) )
4 3 ralbidv ⊢ ( 𝑥 = ∅ → ( ∀ 𝑧 ∈ ω ( 𝑥 ≈ 𝑧 → 𝑥 = 𝑧 ) ↔ ∀ 𝑧 ∈ ω ( ∅ ≈ 𝑧 → ∅ = 𝑧 ) ) )
5 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝑧 ↔ 𝑦 ≈ 𝑧 ) )
6 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )
7 5 6 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≈ 𝑧 → 𝑥 = 𝑧 ) ↔ ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) )
8 7 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑧 ∈ ω ( 𝑥 ≈ 𝑧 → 𝑥 = 𝑧 ) ↔ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) )
9 breq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ≈ 𝑧 ↔ suc 𝑦 ≈ 𝑧 ) )
10 eqeq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 = 𝑧 ↔ suc 𝑦 = 𝑧 ) )
11 9 10 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ≈ 𝑧 → 𝑥 = 𝑧 ) ↔ ( suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧 ) ) )
12 11 ralbidv ⊢ ( 𝑥 = suc 𝑦 → ( ∀ 𝑧 ∈ ω ( 𝑥 ≈ 𝑧 → 𝑥 = 𝑧 ) ↔ ∀ 𝑧 ∈ ω ( suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧 ) ) )
13 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝑧 ↔ 𝐴 ≈ 𝑧 ) )
14 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑧 ↔ 𝐴 = 𝑧 ) )
15 13 14 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≈ 𝑧 → 𝑥 = 𝑧 ) ↔ ( 𝐴 ≈ 𝑧 → 𝐴 = 𝑧 ) ) )
16 15 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ ω ( 𝑥 ≈ 𝑧 → 𝑥 = 𝑧 ) ↔ ∀ 𝑧 ∈ ω ( 𝐴 ≈ 𝑧 → 𝐴 = 𝑧 ) ) )
17 0fin ⊢ ∅ ∈ Fin
18 ensymfib ⊢ ( ∅ ∈ Fin → ( ∅ ≈ 𝑧 ↔ 𝑧 ≈ ∅ ) )
19 17 18 ax-mp ⊢ ( ∅ ≈ 𝑧 ↔ 𝑧 ≈ ∅ )
20 en0 ⊢ ( 𝑧 ≈ ∅ ↔ 𝑧 = ∅ )
21 eqcom ⊢ ( 𝑧 = ∅ ↔ ∅ = 𝑧 )
22 20 21 bitri ⊢ ( 𝑧 ≈ ∅ ↔ ∅ = 𝑧 )
23 19 22 sylbb ⊢ ( ∅ ≈ 𝑧 → ∅ = 𝑧 )
24 23 rgenw ⊢ ∀ 𝑧 ∈ ω ( ∅ ≈ 𝑧 → ∅ = 𝑧 )
25 nn0suc ⊢ ( 𝑤 ∈ ω → ( 𝑤 = ∅ ∨ ∃ 𝑧 ∈ ω 𝑤 = suc 𝑧 ) )
26 en0 ⊢ ( suc 𝑦 ≈ ∅ ↔ suc 𝑦 = ∅ )
27 breq2 ⊢ ( 𝑤 = ∅ → ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ ∅ ) )
28 eqeq2 ⊢ ( 𝑤 = ∅ → ( suc 𝑦 = 𝑤 ↔ suc 𝑦 = ∅ ) )
29 27 28 bibi12d ⊢ ( 𝑤 = ∅ → ( ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤 ) ↔ ( suc 𝑦 ≈ ∅ ↔ suc 𝑦 = ∅ ) ) )
30 26 29 mpbiri ⊢ ( 𝑤 = ∅ → ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤 ) )
31 30 biimpd ⊢ ( 𝑤 = ∅ → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) )
32 31 a1i ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑤 = ∅ → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
33 nfv ⊢ Ⅎ 𝑧 𝑦 ∈ ω
34 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 )
35 33 34 nfan ⊢ Ⅎ 𝑧 ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) )
36 nfv ⊢ Ⅎ 𝑧 ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 )
37 vex ⊢ 𝑦 ∈ V
38 37 phplem2 ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 ≈ 𝑧 ) )
39 38 imim1d ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧 ) ) )
40 39 ex ⊢ ( 𝑦 ∈ ω → ( 𝑧 ∈ ω → ( ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧 ) ) ) )
41 40 a2d ⊢ ( 𝑦 ∈ ω → ( ( 𝑧 ∈ ω → ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑧 ∈ ω → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧 ) ) ) )
42 rsp ⊢ ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( 𝑧 ∈ ω → ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) )
43 41 42 impel ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑧 ∈ ω → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧 ) ) )
44 suceq ⊢ ( 𝑦 = 𝑧 → suc 𝑦 = suc 𝑧 )
45 43 44 syl8 ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑧 ∈ ω → ( suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧 ) ) )
46 breq2 ⊢ ( 𝑤 = suc 𝑧 → ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ suc 𝑧 ) )
47 eqeq2 ⊢ ( 𝑤 = suc 𝑧 → ( suc 𝑦 = 𝑤 ↔ suc 𝑦 = suc 𝑧 ) )
48 46 47 imbi12d ⊢ ( 𝑤 = suc 𝑧 → ( ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ↔ ( suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧 ) ) )
49 48 biimprcd ⊢ ( ( suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧 ) → ( 𝑤 = suc 𝑧 → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
50 45 49 syl6 ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑧 ∈ ω → ( 𝑤 = suc 𝑧 → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) ) )
51 35 36 50 rexlimd ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( ∃ 𝑧 ∈ ω 𝑤 = suc 𝑧 → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
52 32 51 jaod ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( ( 𝑤 = ∅ ∨ ∃ 𝑧 ∈ ω 𝑤 = suc 𝑧 ) → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
53 52 ex ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( ( 𝑤 = ∅ ∨ ∃ 𝑧 ∈ ω 𝑤 = suc 𝑧 ) → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) ) )
54 25 53 syl7 ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( 𝑤 ∈ ω → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) ) )
55 54 ralrimdv ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ∀ 𝑤 ∈ ω ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
56 breq2 ⊢ ( 𝑤 = 𝑧 → ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ 𝑧 ) )
57 eqeq2 ⊢ ( 𝑤 = 𝑧 → ( suc 𝑦 = 𝑤 ↔ suc 𝑦 = 𝑧 ) )
58 56 57 imbi12d ⊢ ( 𝑤 = 𝑧 → ( ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ↔ ( suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧 ) ) )
59 58 cbvralvw ⊢ ( ∀ 𝑤 ∈ ω ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ↔ ∀ 𝑧 ∈ ω ( suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧 ) )
60 55 59 syl6ib ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ∀ 𝑧 ∈ ω ( suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧 ) ) )
61 4 8 12 16 24 60 finds ⊢ ( 𝐴 ∈ ω → ∀ 𝑧 ∈ ω ( 𝐴 ≈ 𝑧 → 𝐴 = 𝑧 ) )
62 breq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 ≈ 𝑧 ↔ 𝐴 ≈ 𝐵 ) )
63 eqeq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 = 𝑧 ↔ 𝐴 = 𝐵 ) )
64 62 63 imbi12d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ≈ 𝑧 → 𝐴 = 𝑧 ) ↔ ( 𝐴 ≈ 𝐵 → 𝐴 = 𝐵 ) ) )
65 64 rspcv ⊢ ( 𝐵 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝐴 ≈ 𝑧 → 𝐴 = 𝑧 ) → ( 𝐴 ≈ 𝐵 → 𝐴 = 𝐵 ) ) )
66 61 65 mpan9 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 → 𝐴 = 𝐵 ) )
67 enrefnn ⊢ ( 𝐴 ∈ ω → 𝐴 ≈ 𝐴 )
68 breq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≈ 𝐴 ↔ 𝐴 ≈ 𝐵 ) )
69 67 68 syl5ibcom ⊢ ( 𝐴 ∈ ω → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )
70 69 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )
71 66 70 impbid ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) )