Add Myhill isomorphism theorem to iset.mm

[jkingdon]

This is sometimes described as a constructive version of https://us.metamath.org/mpeuni/sbth.html

We would:

• Figure out what notation to use.
  • We might define notation for reductions or maybe the definition of a reduction can be expanded inline
  • I suppose expressing reductions however we choose and combining with -->, -1-1->, and -1-1-onto-> may suffice for the analogues to ≼ and ≈ used in expressing the Myhill property
  • Perhaps X e. Myhill would be suitable notation for "X has the Myhill property"? Then _om e. Myhill would express the usual Myhill isomorphism theorem and we could pose questions like NN+oo e. Myhill or the strength of A. x x e. Myhill .
• Show that NN (or _om) has the Myhill property
  • Wikipedia has a sketch of the proof which would resemble the https://us.metamath.org/mpeuni/sbth.html proof apparently.
• Show that a set satisfying https://us.metamath.org/ileuni/df-fin.html has the Myhill property

Sources:

• https://mathstodon.xyz/@andrejbauer/114427716438955347 post by Andrej Bauer
• https://en.wikipedia.org/wiki/Myhill_isomorphism_theorem