add Word to iset.mm (#4984)

* Add Word to iset.mm

This is the syntax and df-word .  Copied without change from set.mm.

* Add iswrd to iset.mm

Stated as in set.mm.  The proof needs a small change for set existence
but is basically the set.mm proof.

* Add wrdval to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
small changes around set existence.

* Add iswrdinn0 to iset.mm

This is iswrdi from set.mm with an additional condition.  The set.mm
proof uses excluded middle to handle the case where -. L e. NN0
so just handle the L e. NN0 case.

* copy wrdf from set.mm to iset.mm

* Add iswrdb to mmil.html

* copy wrddm from set.mm to iset.mm

* Add sswrd to iset.mm

Stated as in set.mm.  The proof is somewhat like the set.mm proof but
more elaborate because iset.mm doesn't have iswrdb .

* Add snopiswrd to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
small changes to use iswrdinn0 in place of iswrdi .

* Add wrdexg to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but set
existence in one spot needs a lot more steps.

* Add wrdexb to iset.mm

Stated as in set.mm.  The proof needs a very small change for set
existence but is otherwise the set.mm proof.

* copy wrdexi from set.mm to iset.mm

* copy wrdsymbcl from set.mm to iset.mm

* copy wrdfn from set.mm to iset.mm

* copy wrdv from set.mm to iset.mm

* copy wrdlndm from set.mm to iset.mm

* Add lencl to iset.mm

Stated as in set.mm.  The proof is different from the set.mm proof
because the set.mm proof uses finite set theorrems not available
in iset.mm.

Also put it slightly earlier in the file as it will be needed in places
that set.mm does not need it.

* Add iswrdsymb to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
small changes to use iswrdinn0 instead of iswrdi .

* Add wrdfin to iset.mm

Stated as in set.mm.  The proof needs to be changed to use fzofig in
place of fzofi but is otherwise the set.mm proof.

* Trim word comments

This is to remove references to theorems that iset.mm doesn't have.
Some of them it is likely to have eventually but not just now.

* copy lennncl from set.mm to iset.mm

* copy wrdffz from set.mm to iset.mm

* copy wrdeq from set.mm to iset.mm

* copy wrdeqi from set.mm to iset.mm

* Add iswrddm0 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with small changes
to use iswrdinn0 .

* copy wrd0 from set.mm to iset.mm

* copy 0wrd0 from set.mm to iset.mm

* add ffz0iswrd to mmil.html

* copy fimadmfo from set.mm to iset.mm

* Add wrdsymb to iset.mm

Stated as in set.mm.  The proof needs small adjustments for Word
theorems but is basically the set.mm proof.

* Rename nfrexxy to nfrexw in iset.mm

This is to better reflect current set.mm naming.  The statement of the
theorems is the same (including distinct variables).

* copy nfwrd from set.mm to iset.mm

* add sbcel2 to mmil.html

* add csbab to mmil.html

* Add csbwrdg to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
small changes for set existence.

* Add wrdnval to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a few changes
for set existence and Word theorems.

* copy wrdmap from set.mm to iset.mm

* add hashwrdn to mmil.html

* add wrdnfi to mmil.html

* Add nelfzo to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
a few changes to show some propositions are decidable.

* Add wrdsymb0 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with some changes
for differences in function value theorems.

* Add wrdlenge1n0 to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof, but needs
small adjustments for differences in set size theorems.

* copy len0nnbi from set.mm to iset.mm

* copy wrdlenge2n0 from set.mm to iset.mm

* copy wrdsymb1 from set.mm to iset.mm

* copy wrdlen1 from set.mm to iset.mm

* copy fstwrdne from set.mm to iset.mm

* copy fstwrdne0 from set.mm to iset.mm

* copy eqwrd from set.mm to iset.mm

* Rename nfrabxy to nfrabw in iset.mm

This is to better match set.mm naming.  The theorems are the same
including distinct variables.

* Add nfsbcw to iset.mm

Copied from set.mm with the only change being to comments and removing
the $j usage because iset.mm hasn't quite caught up to set.mm in the
area of axiom usage.

* copy elovmporab from set.mm to iset.mm

* Add elovmporab1w to iset.mm

Stated as in set.mm.  The only change is to comments and removing the $j
usage because the set.mm text does not apply (at least, not as-is).

* Adjust elovmporab1 comments in iset.mm

We don't have elovmporab1 and probably won't get it, so adjust elovmporab1w
comment and mmil.html entry.

* copy elovmpowrd from set.mm to iset.mm

* add elovmpt3imp to mmil.html

* Add elovmptnn0wrd to mmil.html

* Add iswrdiz to iset.mm

This is an analogue to iswrdinn0 but where it is possible to specify a
negative length to mean an empty sequence.

* Add wrdred1 to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
some changes to deal with differences in word theorems.

* Add wrdred1hash to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
some changes for differences in set size theorems.

* Adjust ffz0iswrd entry in mmil.html

Although iswrdinn0 is fairly close, none isn't really bad either as it
is hopefully clear enough how to apply iswrdiz , iswrdinn0 , etc,
depending on the situation.

Author: jkingdon