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 AωBωABA=B

Proof

Step Hyp Ref Expression
1 breq1 x=xzz
2 eqeq1 x=x=z=z
3 1 2 imbi12d x=xzx=zz=z
4 3 ralbidv x=zωxzx=zzωz=z
5 breq1 x=yxzyz
6 eqeq1 x=yx=zy=z
7 5 6 imbi12d x=yxzx=zyzy=z
8 7 ralbidv x=yzωxzx=zzωyzy=z
9 breq1 x=sucyxzsucyz
10 eqeq1 x=sucyx=zsucy=z
11 9 10 imbi12d x=sucyxzx=zsucyzsucy=z
12 11 ralbidv x=sucyzωxzx=zzωsucyzsucy=z
13 breq1 x=AxzAz
14 eqeq1 x=Ax=zA=z
15 13 14 imbi12d x=Axzx=zAzA=z
16 15 ralbidv x=Azωxzx=zzωAzA=z
17 0fin Fin
18 ensymfib Finzz
19 17 18 ax-mp zz
20 en0 zz=
21 eqcom z==z
22 20 21 bitri z=z
23 19 22 sylbb z=z
24 23 rgenw zωz=z
25 nn0suc wωw=zωw=sucz
26 en0 sucysucy=
27 breq2 w=sucywsucy
28 eqeq2 w=sucy=wsucy=
29 27 28 bibi12d w=sucywsucy=wsucysucy=
30 26 29 mpbiri w=sucywsucy=w
31 30 biimpd w=sucywsucy=w
32 31 a1i yωzωyzy=zw=sucywsucy=w
33 nfv zyω
34 nfra1 zzωyzy=z
35 33 34 nfan zyωzωyzy=z
36 nfv zsucywsucy=w
37 vex yV
38 37 phplem2 yωzωsucysuczyz
39 38 imim1d yωzωyzy=zsucysuczy=z
40 39 ex yωzωyzy=zsucysuczy=z
41 40 a2d yωzωyzy=zzωsucysuczy=z
42 rsp zωyzy=zzωyzy=z
43 41 42 impel yωzωyzy=zzωsucysuczy=z
44 suceq y=zsucy=sucz
45 43 44 syl8 yωzωyzy=zzωsucysuczsucy=sucz
46 breq2 w=suczsucywsucysucz
47 eqeq2 w=suczsucy=wsucy=sucz
48 46 47 imbi12d w=suczsucywsucy=wsucysuczsucy=sucz
49 48 biimprcd sucysuczsucy=suczw=suczsucywsucy=w
50 45 49 syl6 yωzωyzy=zzωw=suczsucywsucy=w
51 35 36 50 rexlimd yωzωyzy=zzωw=suczsucywsucy=w
52 32 51 jaod yωzωyzy=zw=zωw=suczsucywsucy=w
53 52 ex yωzωyzy=zw=zωw=suczsucywsucy=w
54 25 53 syl7 yωzωyzy=zwωsucywsucy=w
55 54 ralrimdv yωzωyzy=zwωsucywsucy=w
56 breq2 w=zsucywsucyz
57 eqeq2 w=zsucy=wsucy=z
58 56 57 imbi12d w=zsucywsucy=wsucyzsucy=z
59 58 cbvralvw wωsucywsucy=wzωsucyzsucy=z
60 55 59 syl6ib yωzωyzy=zzωsucyzsucy=z
61 4 8 12 16 24 60 finds AωzωAzA=z
62 breq2 z=BAzAB
63 eqeq2 z=BA=zA=B
64 62 63 imbi12d z=BAzA=zABA=B
65 64 rspcv BωzωAzA=zABA=B
66 61 65 mpan9 AωBωABA=B
67 enrefnn AωAA
68 breq2 A=BAAAB
69 67 68 syl5ibcom AωA=BAB
70 69 adantr AωBωA=BAB
71 66 70 impbid AωBωABA=B