Metamath Proof Explorer


Definition df-ndx

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)

Ref Expression
Assertion df-ndx
|- ndx = ( _I |` NN )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnx
 |-  ndx
1 cid
 |-  _I
2 cn
 |-  NN
3 1 2 cres
 |-  ( _I |` NN )
4 0 3 wceq
 |-  ndx = ( _I |` NN )