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)

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 ensym ⊢ ( ∅ ≈ 𝑧 → 𝑧 ≈ ∅ )
18 en0 ⊢ ( 𝑧 ≈ ∅ ↔ 𝑧 = ∅ )
19 eqcom ⊢ ( 𝑧 = ∅ ↔ ∅ = 𝑧 )
20 18 19 bitri ⊢ ( 𝑧 ≈ ∅ ↔ ∅ = 𝑧 )
21 17 20 sylib ⊢ ( ∅ ≈ 𝑧 → ∅ = 𝑧 )
22 21 rgenw ⊢ ∀ 𝑧 ∈ ω ( ∅ ≈ 𝑧 → ∅ = 𝑧 )
23 nn0suc ⊢ ( 𝑤 ∈ ω → ( 𝑤 = ∅ ∨ ∃ 𝑧 ∈ ω 𝑤 = suc 𝑧 ) )
24 en0 ⊢ ( suc 𝑦 ≈ ∅ ↔ suc 𝑦 = ∅ )
25 breq2 ⊢ ( 𝑤 = ∅ → ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ ∅ ) )
26 eqeq2 ⊢ ( 𝑤 = ∅ → ( suc 𝑦 = 𝑤 ↔ suc 𝑦 = ∅ ) )
27 25 26 bibi12d ⊢ ( 𝑤 = ∅ → ( ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤 ) ↔ ( suc 𝑦 ≈ ∅ ↔ suc 𝑦 = ∅ ) ) )
28 24 27 mpbiri ⊢ ( 𝑤 = ∅ → ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤 ) )
29 28 biimpd ⊢ ( 𝑤 = ∅ → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) )
30 29 a1i ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑤 = ∅ → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
31 nfv ⊢ Ⅎ 𝑧 𝑦 ∈ ω
32 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 )
33 31 32 nfan ⊢ Ⅎ 𝑧 ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) )
34 nfv ⊢ Ⅎ 𝑧 ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 )
35 vex ⊢ 𝑦 ∈ V
36 vex ⊢ 𝑧 ∈ V
37 35 36 phplem4 ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 ≈ 𝑧 ) )
38 37 imim1d ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧 ) ) )
39 38 ex ⊢ ( 𝑦 ∈ ω → ( 𝑧 ∈ ω → ( ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧 ) ) ) )
40 39 a2d ⊢ ( 𝑦 ∈ ω → ( ( 𝑧 ∈ ω → ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑧 ∈ ω → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧 ) ) ) )
41 rsp ⊢ ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( 𝑧 ∈ ω → ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) )
42 40 41 impel ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑧 ∈ ω → ( suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧 ) ) )
43 suceq ⊢ ( 𝑦 = 𝑧 → suc 𝑦 = suc 𝑧 )
44 42 43 syl8 ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑧 ∈ ω → ( suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧 ) ) )
45 breq2 ⊢ ( 𝑤 = suc 𝑧 → ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ suc 𝑧 ) )
46 eqeq2 ⊢ ( 𝑤 = suc 𝑧 → ( suc 𝑦 = 𝑤 ↔ suc 𝑦 = suc 𝑧 ) )
47 45 46 imbi12d ⊢ ( 𝑤 = suc 𝑧 → ( ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ↔ ( suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧 ) ) )
48 47 biimprcd ⊢ ( ( suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧 ) → ( 𝑤 = suc 𝑧 → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
49 44 48 syl6 ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( 𝑧 ∈ ω → ( 𝑤 = suc 𝑧 → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) ) )
50 33 34 49 rexlimd ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( ∃ 𝑧 ∈ ω 𝑤 = suc 𝑧 → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
51 30 50 jaod ⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) ) → ( ( 𝑤 = ∅ ∨ ∃ 𝑧 ∈ ω 𝑤 = suc 𝑧 ) → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
52 51 ex ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( ( 𝑤 = ∅ ∨ ∃ 𝑧 ∈ ω 𝑤 = suc 𝑧 ) → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) ) )
53 23 52 syl7 ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ( 𝑤 ∈ ω → ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) ) )
54 53 ralrimdv ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ∀ 𝑤 ∈ ω ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ) )
55 breq2 ⊢ ( 𝑤 = 𝑧 → ( suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ 𝑧 ) )
56 eqeq2 ⊢ ( 𝑤 = 𝑧 → ( suc 𝑦 = 𝑤 ↔ suc 𝑦 = 𝑧 ) )
57 55 56 imbi12d ⊢ ( 𝑤 = 𝑧 → ( ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ↔ ( suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧 ) ) )
58 57 cbvralvw ⊢ ( ∀ 𝑤 ∈ ω ( suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤 ) ↔ ∀ 𝑧 ∈ ω ( suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧 ) )
59 54 58 syl6ib ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝑦 ≈ 𝑧 → 𝑦 = 𝑧 ) → ∀ 𝑧 ∈ ω ( suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧 ) ) )
60 4 8 12 16 22 59 finds ⊢ ( 𝐴 ∈ ω → ∀ 𝑧 ∈ ω ( 𝐴 ≈ 𝑧 → 𝐴 = 𝑧 ) )
61 breq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 ≈ 𝑧 ↔ 𝐴 ≈ 𝐵 ) )
62 eqeq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 = 𝑧 ↔ 𝐴 = 𝐵 ) )
63 61 62 imbi12d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ≈ 𝑧 → 𝐴 = 𝑧 ) ↔ ( 𝐴 ≈ 𝐵 → 𝐴 = 𝐵 ) ) )
64 63 rspcv ⊢ ( 𝐵 ∈ ω → ( ∀ 𝑧 ∈ ω ( 𝐴 ≈ 𝑧 → 𝐴 = 𝑧 ) → ( 𝐴 ≈ 𝐵 → 𝐴 = 𝐵 ) ) )
65 60 64 mpan9 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 → 𝐴 = 𝐵 ) )
66 eqeng ⊢ ( 𝐴 ∈ ω → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )
67 66 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )
68 65 67 impbid ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) )