Announcing an additional Metamath 100 Theorem for iset.mm

[Jim Kingdon]

I am pleased to report the successful completion of the project to
formalize the equinumerosity of the rationals and the natural numbers in
iset.mm.[1]  This project was begun in earnest in May 2022 with the
opening of a github issue[2] which quickly led to discussions and
partial results followed by steady progress leading to this result.

Some of the results along the way included:

* realizing that decomposing a natural number into a power of two and an
odd divisor could be an important part of the proof,[3]

* defining omniscient set notation and theorems

* defining disjoint union notation and theorems

* two impossibility proofs about the Schroeder-Bernstein theorem, the
full theorem (formalizing a 2019 paper) and a special case (we have an
impossibility proof of the special case but just how strong it is
appears to be an open problem[4]),

* a variety of theorems about countable sets ( for example [5]), and

* an example of a novel way (novel as far as I noticed, anyway) to use
the seq notation to define a family of functions both in terms of the
previous member of the family and the index within the collection[6]

Many thanks to everyone who collaborated on this, especially Mario
Carneiro, Thierry Arnoux, and Benoit Jubin (and probably others I'm
forgetting to mention). I never could have done something like this by
myself.

I'd also like to make a special acknowledgement to Peter Aczel[7] who
with a coauthor wrote the textbook which contained the key lemma for
this proof[8]. He died on August 1, 2023 and was a great mathematician
and person according to all the tributes I read on Mastodon from people
who had worked with him.

[1] https://us.metamath.org/ileuni/qnnen.html

[2] https://github.com/metamath/set.mm/issues/2595

[3] https://us.metamath.org/ileuni/oddpwdc.html

[4]
https://mathoverflow.net/questions/451785/how-strong-is-the-schr%c3%b6der-bernstein-theorem-where-one-set-is-the-natural-number

[5] https://us.metamath.org/ileuni/ctm.html

[6] https://us.metamath.org/ileuni/ennnfonelemen.html and other lemmas
using the hypotheses here

[7] https://en.wikipedia.org/wiki/Peter_Aczel

[8] https://us.metamath.org/ileuni/ennnfone.html , Corollary 8.1.13 in
the cited textbook