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 | |
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 | |
|
10 | eqeq1 | |
|
11 | 9 10 | imbi12d | |
12 | 11 | ralbidv | |
13 | breq1 | |
|
14 | eqeq1 | |
|
15 | 13 14 | imbi12d | |
16 | 15 | ralbidv | |
17 | 0fin | |
|
18 | ensymfib | |
|
19 | 17 18 | ax-mp | |
20 | en0 | |
|
21 | eqcom | |
|
22 | 20 21 | bitri | |
23 | 19 22 | sylbb | |
24 | 23 | rgenw | |
25 | nn0suc | |
|
26 | en0 | |
|
27 | breq2 | |
|
28 | eqeq2 | |
|
29 | 27 28 | bibi12d | |
30 | 26 29 | mpbiri | |
31 | 30 | biimpd | |
32 | 31 | a1i | |
33 | nfv | |
|
34 | nfra1 | |
|
35 | 33 34 | nfan | |
36 | nfv | |
|
37 | vex | |
|
38 | 37 | phplem2 | |
39 | 38 | imim1d | |
40 | 39 | ex | |
41 | 40 | a2d | |
42 | rsp | |
|
43 | 41 42 | impel | |
44 | suceq | |
|
45 | 43 44 | syl8 | |
46 | breq2 | |
|
47 | eqeq2 | |
|
48 | 46 47 | imbi12d | |
49 | 48 | biimprcd | |
50 | 45 49 | syl6 | |
51 | 35 36 50 | rexlimd | |
52 | 32 51 | jaod | |
53 | 52 | ex | |
54 | 25 53 | syl7 | |
55 | 54 | ralrimdv | |
56 | breq2 | |
|
57 | eqeq2 | |
|
58 | 56 57 | imbi12d | |
59 | 58 | cbvralvw | |
60 | 55 59 | syl6ib | |
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 | |