Add dist, le and UnifSet slots to CCfld in iset.mm (#5029)

* Change distinct variables for mpofvex in iset.mm

This is removing the $d B x $. condition for both mpofvex and mpofvexi .
Not only is it not needed (the proof doesn't use it), but there are a
number of places where we have B depend on x (see especially mpoxeldm
and the section containing it, or for an example df-fg ).

Also applies to mpofvexi .

* Add metuex to iset.mm.

This is a set existence theorem of the sort that we need because we
don't have ovex .  The proof is via set existence theorems such as
mpofvexi and mptfvex .

* Add cndsex to iset.mm

This is a simple set existence theorem.  The proof is taken from a
portion of the cntopex proof.  Revise the cntopex proof to refer to
cndsex .

* Change CCfld definition in iset.mm

Copy df-cnfld from set.mm and replace df-icnfld with it.  The only change
is a small one to the comment.

Revise proofs of cnfldstr , cnfldbas , mpocnfldadd , mpocnfldmul ,
cnfldcj and , cnfldtset accordingly.  They need to account for the new
slots but are otherwise similar to the previous iset.mm proofs.

Add cnfldle and cnfldds to iset.mm.  Stated as in set.mm (with the
proof being the set.mm proof, slightly modified).

Update mmil.html accordingly

* copy cnfldms from set.mm to iset.mm

* copy cnfldxms from set.mm to iset.mm

* copy cnfldtps from set.mm to iset.mm

* copy cnfldtopn from set.mm to iset.mm

* copy cnfldtopon from set.mm to iset.mm

* copy cnfldtop from set.mm to iset.mm

* copy unicntop from set.mm to iset.mm

* copy cnopn from set.mm to iset.mm

* copy tgioo2 from set.mm to iset.mm

* copy rerest from set.mm to iset.mm

Author: jkingdon

iset-discouraged

@@ -158,14 +158,16 @@
 "dcan2" is used by "nninfdclemp1".
 "dcan2" is used by "nninfsellemdc".
 "dcan2" is used by "pcmptdvds".
+"df-cnfld" is used by "cnfldbas".
+"df-cnfld" is used by "cnfldcj".
+"df-cnfld" is used by "cnfldds".
+"df-cnfld" is used by "cnfldle".
+"df-cnfld" is used by "cnfldstr".
+"df-cnfld" is used by "cnfldtset".
+"df-cnfld" is used by "mpocnfldadd".
+"df-cnfld" is used by "mpocnfldmul".
 "df-div" is used by "divfnzn".
 "df-div" is used by "divvalap".
-"df-icnfld" is used by "cnfldbas".
-"df-icnfld" is used by "cnfldcj".
-"df-icnfld" is used by "cnfldstr".
-"df-icnfld" is used by "cnfldtset".
-"df-icnfld" is used by "mpocnfldadd".
-"df-icnfld" is used by "mpocnfldmul".
 "df-ilim" is used by "dflim2".
 "df-inn" is used by "dfnn2".
 "df-iom" is used by "dfom3".
@@ -332,6 +334,7 @@
 "strnfvn" is used by "ndxarg".
 "strnfvn" is used by "strsl0".
 "unifndx" is used by "basendxltunifndx".
+"unifndx" is used by "cnfldstr".
 "unifndx" is used by "slotsdifunifndx".
 "unifndx" is used by "unifndxnn".
 "unifndx" is used by "unifndxntsetndx".
@@ -439,8 +442,8 @@ New usage of "dcan2" is discouraged (11 uses).
 New usage of "dcapnconstALT" is discouraged (0 uses).
 New usage of "dcnnOLD" is discouraged (0 uses).
 New usage of "demoivreALT" is discouraged (0 uses).
+New usage of "df-cnfld" is discouraged (8 uses).
 New usage of "df-div" is discouraged (2 uses).
-New usage of "df-icnfld" is discouraged (6 uses).
 New usage of "df-ilim" is discouraged (1 uses).
 New usage of "df-inn" is discouraged (1 uses).
 New usage of "df-iom" is discouraged (1 uses).
@@ -500,7 +503,7 @@ New usage of "stoic2b" is discouraged (0 uses).
 New usage of "strcollnfALT" is discouraged (0 uses).
 New usage of "strnfvn" is discouraged (3 uses).
 New usage of "tfri1dALT" is discouraged (0 uses).
-New usage of "unifndx" is discouraged (4 uses).
+New usage of "unifndx" is discouraged (5 uses).
 New usage of "uzind4ALT" is discouraged (0 uses).
 New usage of "xpexgALT" is discouraged (0 uses).
 Proof modification of "0cnALT" is discouraged (49 steps).