Description: Define the structure component index extractor. See Theorem ndxarg to
understand its purpose. The restriction to NN ensures that ndx is
a set. The restriction to some set is necessary since _I is a proper
class. In principle, we could have chosen CC or (if we revise all
structure component definitions such as df-base ) another set such as
the set of finite ordinals _om ( df-om ). (Contributed by NM, 4-Sep-2011)