Theorem nneneq 6799

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.)

Assertion

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

Proof of Theorem nneneq

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 3968	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑥 ≈ 𝑧 ↔ ∅ ≈ 𝑧))
2		eqeq1 2164	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑥 = 𝑧 ↔ ∅ = 𝑧))
3	1, 2	imbi12d 233	. . . . 5 ⊢ (𝑥 = ∅ → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (∅ ≈ 𝑧 → ∅ = 𝑧)))
4	3	ralbidv 2457	. . . 4 ⊢ (𝑥 = ∅ → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (∅ ≈ 𝑧 → ∅ = 𝑧)))
5		breq1 3968	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑧 ↔ 𝑦 ≈ 𝑧))
6		eqeq1 2164	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
7	5, 6	imbi12d 233	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)))
8	7	ralbidv 2457	. . . 4 ⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)))
9		breq1 3968	. . . . . 6 ⊢ (𝑥 = suc 𝑦 → (𝑥 ≈ 𝑧 ↔ suc 𝑦 ≈ 𝑧))
10		eqeq1 2164	. . . . . 6 ⊢ (𝑥 = suc 𝑦 → (𝑥 = 𝑧 ↔ suc 𝑦 = 𝑧))
11	9, 10	imbi12d 233	. . . . 5 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧)))
12	11	ralbidv 2457	. . . 4 ⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧)))
13		breq1 3968	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑧 ↔ 𝐴 ≈ 𝑧))
14		eqeq1 2164	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝑧 ↔ 𝐴 = 𝑧))
15	13, 14	imbi12d 233	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (𝐴 ≈ 𝑧 → 𝐴 = 𝑧)))
16	15	ralbidv 2457	. . . 4 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (𝐴 ≈ 𝑧 → 𝐴 = 𝑧)))
17		ensym 6723	. . . . . 6 ⊢ (∅ ≈ 𝑧 → 𝑧 ≈ ∅)
18		en0 6737	. . . . . . 7 ⊢ (𝑧 ≈ ∅ ↔ 𝑧 = ∅)
19		eqcom 2159	. . . . . . 7 ⊢ (𝑧 = ∅ ↔ ∅ = 𝑧)
20	18, 19	bitri 183	. . . . . 6 ⊢ (𝑧 ≈ ∅ ↔ ∅ = 𝑧)
21	17, 20	sylib 121	. . . . 5 ⊢ (∅ ≈ 𝑧 → ∅ = 𝑧)
22	21	rgenw 2512	. . . 4 ⊢ ∀𝑧 ∈ ω (∅ ≈ 𝑧 → ∅ = 𝑧)
23		nn0suc 4562	. . . . . . 7 ⊢ (𝑤 ∈ ω → (𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧))
24		en0 6737	. . . . . . . . . . . 12 ⊢ (suc 𝑦 ≈ ∅ ↔ suc 𝑦 = ∅)
25		breq2 3969	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ ∅))
26		eqeq2 2167	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∅ → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = ∅))
27	25, 26	bibi12d 234	. . . . . . . . . . . 12 ⊢ (𝑤 = ∅ → ((suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ ∅ ↔ suc 𝑦 = ∅)))
28	24, 27	mpbiri 167	. . . . . . . . . . 11 ⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤))
29	28	biimpd 143	. . . . . . . . . 10 ⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))
30	29	a1i 9	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))
31		nfv 1508	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑦 ∈ ω
32		nfra1 2488	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)
33	31, 32	nfan 1545	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑦 ∈ ω ∧ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧))
34		nfv 1508	. . . . . . . . . 10 ⊢ Ⅎ𝑧(suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)
35		rsp 2504	. . . . . . . . . . . . . 14 ⊢ (∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (𝑧 ∈ ω → (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)))
36		vex 2715	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑦 ∈ V
37		vex 2715	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ V
38	36, 37	phplem4 6797	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (suc 𝑦 ≈ suc 𝑧 → 𝑦 ≈ 𝑧))
39	38	imim1d 75	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → ((𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧)))
40	39	ex 114	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ω → (𝑧 ∈ ω → ((𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧))))
41	40	a2d 26	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ω → ((𝑧 ∈ ω → (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧))))
42	35, 41	syl5 32	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧))))
43	42	imp 123	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ω ∧ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧)))
44		suceq 4362	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
45	43, 44	syl8 71	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧)))
46		breq2 3969	. . . . . . . . . . . . 13 ⊢ (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ suc 𝑧))
47		eqeq2 2167	. . . . . . . . . . . . 13 ⊢ (𝑤 = suc 𝑧 → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = suc 𝑧))
48	46, 47	imbi12d 233	. . . . . . . . . . . 12 ⊢ (𝑤 = suc 𝑧 → ((suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧)))
49	48	biimprcd 159	. . . . . . . . . . 11 ⊢ ((suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧) → (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))
50	45, 49	syl6 33	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))))
51	33, 34, 50	rexlimd 2571	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (∃𝑧 ∈ ω 𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))
52	30, 51	jaod 707	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → ((𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧) → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))
53	52	ex 114	. . . . . . 7 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ((𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧) → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))))
54	23, 53	syl7 69	. . . . . 6 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (𝑤 ∈ ω → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))))
55	54	ralrimdv 2536	. . . . 5 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ∀𝑤 ∈ ω (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))
56		breq2 3969	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ 𝑧))
57		eqeq2 2167	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = 𝑧))
58	56, 57	imbi12d 233	. . . . . 6 ⊢ (𝑤 = 𝑧 → ((suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧)))
59	58	cbvralv 2680	. . . . 5 ⊢ (∀𝑤 ∈ ω (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) ↔ ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))
60	55, 59	syl6ib 160	. . . 4 ⊢ (𝑦 ∈ ω → (∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧)))
61	4, 8, 12, 16, 22, 60	finds 4558	. . 3 ⊢ (𝐴 ∈ ω → ∀𝑧 ∈ ω (𝐴 ≈ 𝑧 → 𝐴 = 𝑧))
62		breq2 3969	. . . . 5 ⊢ (𝑧 = 𝐵 → (𝐴 ≈ 𝑧 ↔ 𝐴 ≈ 𝐵))
63		eqeq2 2167	. . . . 5 ⊢ (𝑧 = 𝐵 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐵))
64	62, 63	imbi12d 233	. . . 4 ⊢ (𝑧 = 𝐵 → ((𝐴 ≈ 𝑧 → 𝐴 = 𝑧) ↔ (𝐴 ≈ 𝐵 → 𝐴 = 𝐵)))
65	64	rspcv 2812	. . 3 ⊢ (𝐵 ∈ ω → (∀𝑧 ∈ ω (𝐴 ≈ 𝑧 → 𝐴 = 𝑧) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵)))
66	61, 65	mpan9 279	. 2 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵))
67		eqeng 6708	. . 3 ⊢ (𝐴 ∈ ω → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵))
68	67	adantr 274	. 2 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵))
69	66, 68	impbid 128	1 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   = wceq 1335   ∈ wcel 2128  ∀wral 2435  ∃wrex 2436  ∅c0 3394   class class class wbr 3965  suc csuc 4325  ωcom 4548   ≈ cen 6680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495  ax-iinf 4546

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-opab 4026  df-tr 4063  df-id 4253  df-iord 4326  df-on 4328  df-suc 4331  df-iom 4549  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-fv 5177  df-er 6477  df-en 6683

This theorem is referenced by:  findcard2  6831  findcard2s  6832  unsnfidcex  6861  unsnfidcel  6862  exmidonfinlem  7123  hashen  10653  hashunlem  10673