Expand basendx comment (metamath#4283)

* Expand basendx comment

This is to describe when to look at indices directly and when not to, in
both set.mm and iset.mm.

* Mention numeric indices in structure header

We can keep some of the details in the basendx comment but the section
header for the extensible structure section does discuss the numeric
indices and so we should mention the issue there and link to the more
detailed discussion.

iset.mm

@@ -138945,7 +138945,9 @@ on a finite (and not necessarily sequential) subset of ` NN ` .  The
   set).  By convention, we normally avoid direct reference to the hard-coded
   numeric index and instead use structure component extractors such as ~ ndxid
   and ~ strslfv .  Using extractors makes it easier to change numeric indices
-  and also makes the components' purpose clearer.
+  and also makes the components' purpose clearer.  See the comment of ~ basendx
+  for more details on numeric indices versus the structure component
+  extractors.
 
   There are many other possible ways to handle structures.  We chose this
   extensible structure approach because this approach (1) results in simpler
@@ -139674,10 +139676,20 @@ is a function if the structure (without the empty set) is a function.
   baseid $p |- Base = Slot ( Base ` ndx ) $=
     ( cbs c1 df-base 1nn ndxid ) ABCDE $.
 
-  $( Index value of the base set extractor.  (Normally it is preferred to work
-     with ` ( Base `` ndx ) ` rather than the hard-coded ` 1 ` in order to make
-     structure theorems portable.  This is an example of how to obtain it when
-     needed.)  (New usage is discouraged.)  (Contributed by Mario Carneiro,
+  $( Index value of the base set extractor.
+
+     Use of this theorem is discouraged since the particular value ` 1 ` for
+     the index is an implementation detail.  It is generally sufficient to work
+     with ` ( Base `` ndx ) ` and use theorems such as ~ baseid and
+     ~ basendxnn .
+
+     The main circumstance in which it is necessary to look at indices directly
+     is when showing that a set of indices are disjoint, in proofs such as
+     ~ lmodstrd .  Although we have a few theorems such as ~ basendxnplusgndx ,
+     we do not intend to add such theorems for every pair of indices (which
+     would be quadradically many in the number of indices).
+
+     (New usage is discouraged.)  (Contributed by Mario Carneiro,
      2-Aug-2013.) $)
   basendx $p |- ( Base ` ndx ) = 1 $=
     ( cbs c1 df-base 1nn ndxarg ) ABCDE $.

set.mm

@@ -197309,7 +197309,8 @@ on a finite (and not necessarily sequential) subset of ` NN ` .  The
   ~ ndxid , we can refer to a specific poset with base set ` B ` and order
   relation ` L ` using the extensible structure
   ` { <. ( Base `` ndx ) , B >. , <. ( le `` ndx ) , L >. } ` rather than
-  ` { <. 1 , B >. , <. ; 1 0 , L >. } ` .
+  ` { <. 1 , B >. , <. ; 1 0 , L >. } ` .  See the comment of ~ basendx for
+  more details on numeric indices versus the structure component extractors.
 
   There are many other possible ways to handle structures.  We chose this
   extensible structure approach because this approach (1) results in simpler
@@ -198184,10 +198185,20 @@ is a function if the structure (without the empty set) is a function.
       ( wcel cvv elbasov simpld ) FAJEKJBKJFACDEBIGHLM $.
   $}
 
-  $( Index value of the base set extractor.  (Normally it is preferred to work
-     with ` ( Base `` ndx ) ` rather than the hard-coded ` 1 ` in order to make
-     structure theorems portable.  This is an example of how to obtain it when
-     needed.)  (New usage is discouraged.)  (Contributed by Mario Carneiro,
+  $( Index value of the base set extractor.
+
+     Use of this theorem is discouraged since the particular value ` 1 ` for
+     the index is an implementation detail.  It is generally sufficient to work
+     with ` ( Base `` ndx ) ` and use theorems such as ~ baseid and
+     ~ basendxnn .
+
+     The main circumstance in which it is necessary to look at indices directly
+     is when showing that a set of indices are disjoint, in proofs such as
+     ~ lmodstr .  Although we have a few theorems such as ~ basendxnplusgndx ,
+     we do not intend to add such theorems for every pair of indices (which
+     would be quadradically many in the number of indices).
+
+     (New usage is discouraged.)  (Contributed by Mario Carneiro,
      2-Aug-2013.) $)
   basendx $p |- ( Base ` ndx ) = 1 $=
     ( cbs c1 df-base 1nn ndxarg ) ABCDE $.