Add first part of section "Open sets of a metric space" to iset.mm (#3167)

* Add mopnval to iset.mm

Stated as in set.mm.  The proof needs intuitionizing in several places
but it falls into the usual categories like showing set existence and
replacing fvex .

* Add mopntopon to iset.mm

Copied without change from set.mm.

* Add mopntop and mopnuni to iset.mm

Copied without change from set.mm.

* Add elmopn and mopnfss to iset.mm

Copied without change from set.mm.

* Add mopnm , elmopn2 , and mopnss to iset.mm

Copied without change from set.mm.

* Add isxms to iset.mm

Copied without change from set.mm.

* Add mopnrel to iset.mm

This is intended for use with relelfvdm (unlike in set.mm which has
elfvdm ).  The proof is easy.

* Add isxms2 to iset.mm

Stated as in set.mm.  The proof needs a little bit of intuitionizing but
is basically the set.mm proof.

* Add isms and isms2 to iset.mm

Copied without change from set.mm.

* Add xmstopn and mstopn to iset.mm

Copied without change from set.mm.

* Add xmstps , msxms , and mstps to iset.mm

Copied without change from set.mm.

* Add xmsxmet , msmet , and msf to iset.mm

Copied without change from set.mm.

* Add xmsxmet2 and msmet2 to iset.mm

Copied without change from set.mm.

* Add mscl and xmscl to iset.mm

Copied without change from set.mm.

* Add xmsge0 and xmseq0 to iset.mm

Copied without change from set.mm.

* Add xmssym to iset.mm

Copied without change from set.mm.

* Add metric space triangle inequality to iset.mm

This is xmstri2 , mstri2 , xmstri , mstri , xmstri3 , mstri3 , and
msrtri .  Copied without change from set.mm.

* Add xmspropd and mspropd to iset.mm

Copied without change from set.mm

* Add setsmsbasg to iset.mm

This is setsmsbas from set.mm with additional set existence hypotheses.
The proof is similar to the set.mm proof.

Update iset-discouraged for the additional usage of basendx .  Because
we are using it to show that ( Base ` ndx ) =/= ( TopSet ` ndx ) we need
to look at the index one way or another.

* Add dsndx and dsid to iset.mm

Copied without change from set.mm.

* Add dsslid to iset.mm

Similar to analogous theorems for other slots.

* Add setsmsdsg to iset.mm

This is setsmsds from set.mm with additional set existence hypotheses
and some intuitionizing.

* Document "g" convention in iset.mm

For a long time this has been similar to the set.mm usage but extends it
in at least one way.  So describe that in the iset.mm conventions.

* Add setsmstsetg to iset.mm

This is setsmstset from set.mm with an added set existence condition
for ( MetOpen ` D ) .  The proof is the set.mm one with minor
adjustments.

* Add metric space theorems to mmil.html

This is setsmstopn , setsxms , setsms , tmsval , tmslem , tmsbas ,
+  tmsds , tmstopn , tmsxms , and tmsms .  None of them copy from
set.mm as-is.

* Add entries to mmil.html

This is df-qtop , df-imas , df-qus , df-xps

* Add mopni to iset.mm

Copied without change from set.mm.

* Add mopni2 to iset.mm

Copied without change from set.mm

* Add mopni3 and blssopn to iset.mm

Copied without change from set.mm.

* Add unimopn and mopnin to iset.mm

Copied without change from set.mm.

* Add mopn0 , rnblopn , and blopn to iset.mm

Copied without change from set.mm.

* Add neibl to iset.mm

Copied without change from set.mm.

* Add blnei to iset.mm

Copied without change from set.mm.

* Add blsscls2 to iset.mm

Copied without change from set.mm.

* Add blcld to mmil.html

* Add blcls to mmil.html

* Add blsscls to mmil.html

* Add metss to iset.mm

Copied without change from set.mm.

* Add metequiv to iset.mm

Copied without change from set.mm.

* Add metequiv2 to iset.mm

Copied without change from set.mm.

* Add metss2lem and metss2 to iset.mm

Copied without change from set.mm.

* Add ge0xaddcl to iset.mm

Copied without change from set.mm.

Remove from missing theorems list in mmil.html.

* Add elfvexd to iset.mm

Basically the same issues as elfvex .

* Add comet to iset.mm

Stated as in set.mm.  The proof requires a small amount of
intuitionizing but is mostly unchanged from the set.mm proof.

* Comment fixes to metric spaces.

This is for some theorems in the section "Open sets of a metric space"
in which the comment is wrong or could be made a bit more explicit or
something.  It is the same changes for set.mm and iset.mm as these
theorems are both places.

Author: jkingdon

iset-discouraged

@@ -101,6 +101,7 @@
 "basendx" is used by "2strstrg".
 "basendx" is used by "lmodstrd".
 "basendx" is used by "rngstrg".
+"basendx" is used by "setsmsbasg".
 "basendx" is used by "topgrpstrd".
 "bj-axemptylem" is used by "bj-axempty".
 "bj-axemptylem" is used by "bj-axempty2".
@@ -348,7 +349,7 @@ New usage of "axpre-mulgt0" is discouraged (0 uses).
 New usage of "axprecex" is discouraged (2 uses).
 New usage of "axresscn" is discouraged (4 uses).
 New usage of "axrnegex" is discouraged (0 uses).
-New usage of "basendx" is discouraged (8 uses).
+New usage of "basendx" is discouraged (9 uses).
 New usage of "baseval" is discouraged (0 uses).
 New usage of "bdcnulALT" is discouraged (0 uses).
 New usage of "bdnthALT" is discouraged (0 uses).